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

Theorem 19.21t 1814
Description: Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
Assertion
Ref Expression
19.21t  |-  ( F/ x ph  ->  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) ) )

Proof of Theorem 19.21t
StepHypRef Expression
1 nfr 1778 . . 3  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
2 ax-5 1567 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
31, 2syl9 69 . 2  |-  ( F/ x ph  ->  ( A. x ( ph  ->  ps )  ->  ( ph  ->  A. x ps )
) )
4 19.9t 1794 . . . 4  |-  ( F/ x ph  ->  ( E. x ph  <->  ph ) )
54imbi1d 310 . . 3  |-  ( F/ x ph  ->  (
( E. x ph  ->  A. x ps )  <->  (
ph  ->  A. x ps )
) )
6 19.38 1813 . . 3  |-  ( ( E. x ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
75, 6syl6bir 222 . 2  |-  ( F/ x ph  ->  (
( ph  ->  A. x ps )  ->  A. x
( ph  ->  ps )
) )
83, 7impbid 185 1  |-  ( F/ x ph  ->  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550   E.wex 1551   F/wnf 1554
This theorem is referenced by:  19.21  1815  nfimd  1828  sbcom  2166  sbcomOLD  2167  sbal2  2213  ax11indalem  2276  ax11inda2ALT  2277  r19.21t  2793  ceqsalt  2980  sbciegft  3193  sbcomwAUX7  29662  sbcomOLD7  29829  sbal2OLD7  29842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator