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

Theorem 19.21 1771
Description: Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in  ph." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
Hypothesis
Ref Expression
19.21.1  |-  F/ x ph
Assertion
Ref Expression
19.21  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )

Proof of Theorem 19.21
StepHypRef Expression
1 19.21.1 . 2  |-  F/ x ph
2 19.21t 1770 . 2  |-  ( F/ x ph  ->  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) ) )
31, 2ax-mp 10 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wal 1532   F/wnf 1539
This theorem is referenced by:  19.21-2  1772  nf3  1779  19.32  1794  nfim1  1805  19.21v  2012  19.12vv  2032  ax15  2104  eu2  2141  moanim  2172  r2alf  2551  19.12b  23513  pm11.53g  24316  a12study2  28285
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540
  Copyright terms: Public domain W3C validator