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

Theorem 19.23v 1832
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 1605 . 2  |-  F/ x ps
2119.23 1797 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527   E.wex 1528
This theorem is referenced by:  19.23vv  1833  2eu4  2226  euind  2952  reuind  2968  r19.3rzv  3547  unissb  3857  disjor  4007  dftr2  4115  ssrelrel  4787  cotr  5055  dffun2  5265  fununi  5316  dff13  5783  dffi2  7176  aceq2  7746  metcld  18731  metcld2  18732  isch2  21803  funcnv5mpt  23236  disjorf  23356  dfon2lem8  24146  psgnunilem4  27420  pm10.52  27560  truniALT  28305  tpid3gVD  28618  truniALTVD  28654  onfrALTVD  28667  unisnALT  28702  bnj1052  29005  bnj1030  29017
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator