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

Theorem 19.23v 1914
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 1819 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549   E.wex 1550
This theorem is referenced by:  19.23vv  1915  2eu4  2363  euind  3113  reuind  3129  r19.3rzv  3713  unissb  4037  disjor  4188  dftr2  4296  ssrelrel  4967  cotr  5237  dffun2  5455  fununi  5508  dff13  5995  dffi2  7419  aceq2  7989  metcld  19246  metcld2  19247  isch2  22714  disjorf  24009  funcnv5mpt  24072  dfon2lem8  25401  psgnunilem4  27335  pm10.52  27475  truniALT  28481  tpid3gVD  28808  truniALTVD  28844  onfrALTVD  28857  unisnALT  28892  bnj1052  29198  bnj1030  29210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator