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

Theorem 19.21 1814
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 1813 . 2  |-  ( F/ x ph  ->  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) ) )
31, 2ax-mp 8 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549   F/wnf 1553
This theorem is referenced by:  19.21h  1815  stdpc5  1816  nfim1OLD  1831  19.21-2  1887  nf3  1890  19.32  1896  19.21v  1913  19.12vv  1921  cbv1  1973  ax15  2107  eu2  2306  moanim  2337  r2alf  2740  19.12b  25429  ax15NEW7  29536  19.12vvOLD7  29701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator