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

Theorem 19.23v 2022
Description: Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
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 nfv 1629 . 2  |-  F/ x ps
2119.23 1777 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wal 1532   E.wex 1537
This theorem is referenced by:  19.23vv  2023  2eu4  2199  euind  2903  reuind  2917  r19.3rzv  3489  unissb  3798  disjor  3947  dftr2  4055  ssrelrel  4740  cotr  5008  dffun2  5169  fununi  5219  dff13  5682  dffi2  7109  aceq2  7679  metcld  18658  metcld2  18659  isch2  21728  dfon2lem8  23480  psgnunilem4  26752  pm10.52  26892  truniALT  27321  tpid3gVD  27631  truniALTVD  27667  onfrALTVD  27680  unisnALT  27715  bnj1052  28017  bnj1030  28029
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator