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

Theorem 19.23v 1932
Description: Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.)
Assertion
Ref Expression
19.23v  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem 19.23v
StepHypRef Expression
1 exim 1633 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 19.9v 1728 . . 3  |-  ( E. x ps  <->  ps )
31, 2syl6ib 226 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  ps )
)
4 ax-5 1680 . . . 4  |-  ( ps 
->  A. x ps )
54imim2i 14 . . 3  |-  ( ( E. x ph  ->  ps )  ->  ( E. x ph  ->  A. x ps ) )
6 19.38 1639 . . 3  |-  ( ( E. x ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
75, 6syl 16 . 2  |-  ( ( E. x ph  ->  ps )  ->  A. x
( ph  ->  ps )
)
83, 7impbii 188 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  19.23vv  1934  2mo2  2381  2eu4OLD  2391  euind  3295  reuind  3312  r19.3rzv  3926  unissb  4282  disjor  4436  dftr2  4547  ssrelrel  5108  cotrg  5383  dffun2  5603  fununi  5659  dff13  6164  dffi2  7893  aceq2  8510  psgnunilem4  16372  metcld  21589  metcld2  21590  isch2  25932  disjorf  27231  funcnv5mpt  27302  dfon2lem8  29117  pm10.52  31140  truniALT  32685  tpid3gVD  33015  truniALTVD  33051  onfrALTVD  33064  unisnALT  33099  bnj1052  33403  bnj1030  33415
  Copyright terms: Public domain W3C validator