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

Theorem 19.23v 1807
Description: Version of 19.23 1966 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 1701 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 19.9v 1801 . . 3  |-  ( E. x ps  <->  ps )
31, 2syl6ib 229 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  ps )
)
4 ax-5 1748 . . . 4  |-  ( ps 
->  A. x ps )
54imim2i 16 . . 3  |-  ( ( E. x ph  ->  ps )  ->  ( E. x ph  ->  A. x ps ) )
6 19.38 1707 . . 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 190 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  19.23vv  1808  pm11.53v  1811  equsalvw  1836  2mo2  2346  euind  3258  reuind  3275  r19.3rzv  3890  unissb  4247  disjor  4405  dftr2  4517  ssrelrel  4950  cotrg  5226  dffun2  5607  fununi  5663  dff13  6170  dffi2  7939  aceq2  8550  psgnunilem4  17125  metcld  22261  metcld2  22262  isch2  26861  disjorf  28178  funcnv5mpt  28261  bnj1052  29779  bnj1030  29791  dfon2lem8  30430  elintima  36104  relexp0eq  36152  dfhe3  36227  pm10.52  36571  truniALT  36759  tpid3gVD  37098  truniALTVD  37135  onfrALTVD  37148  unisnALT  37183
  Copyright terms: Public domain W3C validator