Theorem 19.3 1027

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 970	. 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 951

This theorem is referenced by:  19.16 1044  19.17 1045  19.27 1065  19.28 1066  19.37 1076  equsal 1147  2eu4 1445  axrep1 2684  axrep4 2687  kmlem14 4750  zfcndrep 4938  zfcndpow 4940  zfcndac 4943

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain