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
ralsn.2
Assertion
Ref Expression
rexsn
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem rexsn
StepHypRef Expression
1 ralsn.1 . 2
2 ralsn.2 . . 3
32rexsng 4038 . 2
41, 3ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wceq 1437   wcel 1870  wrex 2783  cvv 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