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

Theorem 19.23v 1834
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 1607 . 2  |-  F/ x ps
2119.23 1799 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1529   E.wex 1530
This theorem is referenced by:  19.23vv  1835  2eu4  2228  euind  2954  reuind  2970  r19.3rzv  3549  unissb  3859  disjor  4009  dftr2  4117  ssrelrel  4789  cotr  5057  dffun2  5267  fununi  5318  dff13  5785  dffi2  7178  aceq2  7748  metcld  18733  metcld2  18734  isch2  21805  funcnv5mpt  23238  disjorf  23358  dfon2lem8  24148  psgnunilem4  27431  pm10.52  27571  truniALT  28361  tpid3gVD  28691  truniALTVD  28727  onfrALTVD  28740  unisnALT  28775  bnj1052  29078  bnj1030  29090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-nf 1534
  Copyright terms: Public domain W3C validator