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

Theorem 19.23v 1915
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 1630 . 2  |-  F/ x ps
2119.23 1820 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550   E.wex 1551
This theorem is referenced by:  19.23vv  1916  2eu4  2366  euind  3123  reuind  3139  r19.3rzv  3723  unissb  4047  disjor  4199  dftr2  4307  ssrelrel  4979  cotr  5249  dffun2  5467  fununi  5520  dff13  6007  dffi2  7431  aceq2  8005  metcld  19263  metcld2  19264  isch2  22731  disjorf  24026  funcnv5mpt  24089  dfon2lem8  25422  psgnunilem4  27411  pm10.52  27551  truniALT  28700  tpid3gVD  29028  truniALTVD  29064  onfrALTVD  29077  unisnALT  29112  bnj1052  29418  bnj1030  29430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator