Theorem 19.3 1072

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 1014	. 2 |- (A.xph -> ph)
2		19.3.1	. 2 |- (ph -> A.xph)
3	1, 2	impbii 164	1 |- (A.xph <-> ph)

Syntax hints:   -> wi 3   <-> wb 153  A.wal 995

This theorem is referenced by:  19.16 1089  19.17 1090  19.27 1110  19.28 1111  19.37 1121  equsal 1193  2eu4 1495  axrep1 2749  axrep4 2752  kmlem14 4840  zfcndrep 5031  zfcndpow 5033  zfcndac 5036

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

This theorem depends on definitions:  df-bi 154

Copyright terms: Public domain