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

Theorem rexsn 4069
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:   ,   ,

Proof of Theorem rexsn
StepHypRef Expression
1 ralsn.1 . 2
2 ralsn.2 . . 3
32rexsng 4065 . 2
41, 3ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  E.wrex 2808   cvv 3109  {csn 4029
This theorem is referenced by:  elsnres  5315  oarec  7230  snec  7393  zornn0g  8906  fpwwe2lem13  9041  elreal  9529  vdwlem6  14504  pmatcollpw3fi1  19289  restsn  19671  snclseqg  20614  ust0  20722  eulerpartlemgh  28317  eldm3  29191  heiborlem3  30309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-rex 2813  df-v 3111  df-sbc 3328  df-sn 4030
  Copyright terms: Public domain W3C validator