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
Assertion
Ref Expression
19.3

Proof of Theorem 19.3
StepHypRef Expression
1 sp 1716 . 2
2 19.3.1 . . 3
32nfri 1742 . 2
41, 3impbii 180 1
 Colors of variables: wff set class Syntax hints:   wb 176  wal 1527  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