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

Theorem 19.3 1781
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 1716 . 2  |-  ( A. x ph  ->  ph )
2 19.3.1 . . 3  |-  F/ x ph
32nfri 1742 . 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 1527   F/wnf 1531
This theorem is referenced by:  19.16  1787  19.17  1788  19.27  1805  19.28  1806  19.37  1809  equsal  1900  2eu4  2226  axrep1  4132  axrep4  4135  kmlem14  7789  zfcndrep  8236  zfcndpow  8238  zfcndac  8241  quantriv  24839  dford4  27122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator