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

Theorem 19.3 1760
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 ax-4 1692 . 2  |-  ( A. x ph  ->  ph )
2 19.3.1 . . 3  |-  F/ x ph
32nfri 1703 . 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 1532   F/wnf 1539
This theorem is referenced by:  19.16  1767  19.17  1768  19.27  1786  19.28  1787  19.37  1790  equsal  1851  2eu4  2199  axrep1  4092  axrep4  4095  kmlem14  7743  zfcndrep  8190  zfcndpow  8192  zfcndac  8195  quantriv  24200  dford4  26475
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540
  Copyright terms: Public domain W3C validator