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

Theorem rexsn 4042
Description: Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
Hypotheses
Ref Expression
ralsn.1  |-  A  e. 
_V
ralsn.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rexsn  |-  ( E. x  e.  { A } ph  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rexsn
StepHypRef Expression
1 ralsn.1 . 2  |-  A  e. 
_V
2 ralsn.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32rexsng 4038 . 2  |-  ( A  e.  _V  ->  ( E. x  e.  { A } ph  <->  ps ) )
41, 3ax-mp 5 1  |-  ( E. x  e.  { A } ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1870   E.wrex 2783   _Vcvv 3087   {csn 4002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-rex 2788  df-v 3089  df-sbc 3306  df-sn 4003
This theorem is referenced by:  elsnres  5161  oarec  7271  snec  7434  zornn0g  8933  fpwwe2lem13  9066  elreal  9554  vdwlem6  14899  pmatcollpw3fi1  19743  restsn  20117  snclseqg  21061  ust0  21165  esum2dlem  28752  eulerpartlemgh  29037  eldm3  30189  poimirlem28  31672  heiborlem3  31849
  Copyright terms: Public domain W3C validator