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

Theorem 19.21t 1803
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 1769 . . 3  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
2 ax-5 1563 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
31, 2syl9 68 . 2  |-  ( F/ x ph  ->  ( A. x ( ph  ->  ps )  ->  ( ph  ->  A. x ps )
) )
4 19.9t 1787 . . . 4  |-  ( F/ x ph  ->  ( E. x ph  <->  ph ) )
54imbi1d 309 . . 3  |-  ( F/ x ph  ->  (
( E. x ph  ->  A. x ps )  <->  (
ph  ->  A. x ps )
) )
6 19.38 1802 . . 3  |-  ( ( E. x ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
75, 6syl6bir 221 . 2  |-  ( F/ x ph  ->  (
( ph  ->  A. x ps )  ->  A. x
( ph  ->  ps )
) )
83, 7impbid 184 1  |-  ( F/ x ph  ->  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546   E.wex 1547   F/wnf 1550
This theorem is referenced by:  19.21  1804  nfimd  1817  dvelimv  1975  sbcom  2122  sbal2  2168  ax11indalem  2231  ax11inda2ALT  2232  r19.21t  2734  ceqsalt  2921  sbciegft  3134  sbcomwAUX7  28923  sbcomOLD7  29071  sbal2OLD7  29085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator