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

Theorem 19.23v 1829
Description: Version of 19.23 2004 with a dv condition instead of a non-freeness hypothesis. (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 1717 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 19.9v 1823 . . 3  |-  ( E. x ps  <->  ps )
31, 2syl6ib 234 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  ps )
)
4 ax-5 1769 . . . 4  |-  ( ps 
->  A. x ps )
54imim2i 16 . . 3  |-  ( ( E. x ph  ->  ps )  ->  ( E. x ph  ->  A. x ps ) )
6 19.38 1723 . . 3  |-  ( ( E. x ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
75, 6syl 17 . 2  |-  ( ( E. x ph  ->  ps )  ->  A. x
( ph  ->  ps )
)
83, 7impbii 192 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1453   E.wex 1674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816
This theorem depends on definitions:  df-bi 190  df-ex 1675
This theorem is referenced by:  19.23vv  1830  pm11.53v  1833  equsalvw  1858  2mo2  2390  euind  3237  reuind  3255  r19.3rzv  3874  unissb  4243  disjor  4401  dftr2  4513  ssrelrel  4954  cotrg  5230  dffun2  5611  fununi  5671  dff13  6184  dffi2  7963  aceq2  8576  psgnunilem4  17187  metcld  22324  metcld2  22325  isch2  26925  disjorf  28238  funcnv5mpt  28321  bnj1052  29833  bnj1030  29845  dfon2lem8  30485  bj-ssbeq  31285  bj-ssb0  31286  bj-ssb1a  31290  bj-ssb1  31291  bj-ssbequ2  31301  bj-ssbid2ALT  31304  elmapintrab  36227  elinintrab  36228  undmrnresiss  36255  elintima  36290  relexp0eq  36338  dfhe3  36415  pm10.52  36758  truniALT  36946  tpid3gVD  37278  truniALTVD  37315  onfrALTVD  37328  unisnALT  37363
  Copyright terms: Public domain W3C validator