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  1850  2eu4  2196  axrep1  4029  axrep4  4032  kmlem14  7673  zfcndrep  8116  zfcndpow  8118  zfcndac  8121  quantriv  24013  dford4  26288
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