Theorem 19.3 1031

Description: A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89.

Hypothesis

Ref	Expression
19.3.1	|- (ph -> A.xph)

Assertion

Ref	Expression
19.3	|- (A.xph <-> ph)

Proof of Theorem 19.3

Step	Hyp	Ref	Expression
1		ax-4 973	. 2 |- (A.xph -> ph)
2		19.3.1	. 2 |- (ph -> A.xph)
3	1, 2	impbi 157	1 |- (A.xph <-> ph)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954

This theorem is referenced by:  19.16 1048  19.17 1049  19.27 1069  19.28 1070  19.37 1080  equsal 1151  2eu4 1452  axrep1 2694  axrep4 2697  kmlem14 4770  zfcndrep 4958  zfcndpow 4960  zfcndac 4963

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 973

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain