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

Theorem 19.3 1793
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 1728 . 2  |-  ( A. x ph  ->  ph )
2 19.3.1 . . 3  |-  F/ x ph
32nfri 1754 . 2  |-  ( ph  ->  A. x ph )
41, 3impbii 180 1  |-  ( A. x ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530   F/wnf 1534
This theorem is referenced by:  19.16  1799  19.17  1800  19.27  1817  19.28  1818  19.37  1821  equsal  1913  2eu4  2239  axrep1  4148  axrep4  4151  kmlem14  7805  zfcndrep  8252  zfcndpow  8254  zfcndac  8257  quantriv  24911  dford4  27225  equsalNEW7  29464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator