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

Theorem 19.23v 1903
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 1626 . 2  |-  F/ x ps
2119.23 1809 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546   E.wex 1547
This theorem is referenced by:  19.23vv  1904  2eu4  2321  euind  3064  reuind  3080  r19.3rzv  3664  unissb  3987  disjor  4137  dftr2  4245  ssrelrel  4916  cotr  5186  dffun2  5404  fununi  5457  dff13  5943  dffi2  7363  aceq2  7933  metcld  19129  metcld2  19130  isch2  22574  disjorf  23865  funcnv5mpt  23925  dfon2lem8  25170  psgnunilem4  27089  pm10.52  27229  truniALT  27969  tpid3gVD  28295  truniALTVD  28331  onfrALTVD  28344  unisnALT  28379  bnj1052  28682  bnj1030  28694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator