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

Theorem 19.23v 2021
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  2022  2eu4  2196  euind  2889  reuind  2903  r19.3rzv  3453  unissb  3755  disjor  3904  dftr2  4012  ssrelrel  4694  cotr  4962  dffun2  5123  fununi  5173  dff13  5635  dffi2  7060  aceq2  7630  metcld  18563  metcld2  18564  isch2  21633  dfon2lem8  23314  psgnunilem4  26586  pm10.52  26726  truniALT  26998  tpid3gVD  27308  truniALTVD  27344  onfrALTVD  27357  unisnALT  27392  bnj1052  27694  bnj1030  27706
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