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  2201  euind  2927  reuind  2943  r19.3rzv  3522  unissb  3831  disjor  3981  dftr2  4089  ssrelrel  4775  cotr  5043  dffun2  5204  fununi  5254  dff13  5717  dffi2  7144  aceq2  7714  metcld  18694  metcld2  18695  isch2  21764  dfon2lem8  23516  psgnunilem4  26788  pm10.52  26928  truniALT  27441  tpid3gVD  27751  truniALTVD  27787  onfrALTVD  27800  unisnALT  27835  bnj1052  28137  bnj1030  28149
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