Theorem 19.3 1378

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

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296

This theorem is referenced by:  19.16 1395  19.17 1396  19.27 1419  19.28 1420  19.37 1431  equsal 1511  equsalOLD 1512  2eu4 1856  axrep1 3429  axrep4 3432  kmlem14 5940  zfcndrep 6118  zfcndpow 6120  zfcndac 6123  quantriv 14150

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

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain