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

Proof of Theorem 19.3
StepHypRef Expression
1 ax-4 1692 . 2
2 19.3.1 . . 3
32nfri 1703 . 2
41, 3impbii 182 1
 Colors of variables: wff set class Syntax hints:   wb 178  wal 1532  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