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

Theorem 19.23v 1910
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 1673 . 2  |-  F/ x ps
2119.23 1843 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1367   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590
This theorem is referenced by:  19.23vv  1911  2mo2  2359  2eu4OLD  2369  euind  3145  reuind  3161  r19.3rzv  3772  unissb  4122  disjor  4275  dftr2  4386  ssrelrel  4939  cotr  5209  dffun2  5427  fununi  5483  dff13  5970  dffi2  7672  aceq2  8288  psgnunilem4  16002  metcld  20815  metcld2  20816  isch2  24625  disjorf  25922  funcnv5mpt  25987  dfon2lem8  27602  pm10.52  29615  truniALT  31246  tpid3gVD  31576  truniALTVD  31612  onfrALTVD  31625  unisnALT  31660  bnj1052  31964  bnj1030  31976
  Copyright terms: Public domain W3C validator