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

Theorem 19.23v 1844
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 1609 . 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 176   A.wal 1530   E.wex 1531
This theorem is referenced by:  19.23vv  1845  2eu4  2239  euind  2965  reuind  2981  r19.3rzv  3560  unissb  3873  disjor  4023  dftr2  4131  ssrelrel  4803  cotr  5071  dffun2  5281  fununi  5332  dff13  5799  dffi2  7192  aceq2  7762  metcld  18747  metcld2  18748  isch2  21819  funcnv5mpt  23251  disjorf  23371  dfon2lem8  24217  psgnunilem4  27523  pm10.52  27663  truniALT  28604  tpid3gVD  28934  truniALTVD  28970  onfrALTVD  28983  unisnALT  29018  bnj1052  29321  bnj1030  29333
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator