MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.3 Unicode version

Theorem 19.3 1783
Description: A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
Hypothesis
Ref Expression
19.3.1  |-  F/ x ph
Assertion
Ref Expression
19.3  |-  ( A. x ph  <->  ph )

Proof of Theorem 19.3
StepHypRef Expression
1 sp 1717 . 2  |-  ( A. x ph  ->  ph )
2 19.3.1 . . 3  |-  F/ x ph
32nfri 1744 . 2  |-  ( ph  ->  A. x ph )
41, 3impbii 182 1  |-  ( A. x ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1528   F/wnf 1532
This theorem is referenced by:  19.16  1789  19.17  1790  19.27  1807  19.28  1808  19.37  1811  equsal  1903  2eu4  2228  axrep1  4134  axrep4  4137  kmlem14  7785  zfcndrep  8232  zfcndpow  8234  zfcndac  8237  quantriv  24247  dford4  26522
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-nf 1533
  Copyright terms: Public domain W3C validator