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

Theorem rexsn 3751
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 3749 . 2  |-  ( A  e.  _V  ->  ( E. x  e.  { A } ph  <->  ps ) )
41, 3ax-mp 8 1  |-  ( E. x  e.  { A } ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642    e. wcel 1710   E.wrex 2620   _Vcvv 2864   {csn 3716
This theorem is referenced by:  elsnres  5073  oarec  6647  snec  6809  zornn0g  8222  fpwwe2lem13  8354  elreal  8843  vdwlem6  13130  restsn  17007  snclseqg  17900  ust0  23523  eldm3  24677  rexsnOLD  25667  heiborlem3  25860
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-v 2866  df-sbc 3068  df-sn 3722
  Copyright terms: Public domain W3C validator