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

Theorem rexsng 4065
Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
Hypothesis
Ref Expression
ralsng.1
Assertion
Ref Expression
rexsng
Distinct variable groups:   ,   ,

Proof of Theorem rexsng
StepHypRef Expression
1 rexsns 4062 . 2
2 ralsng.1 . . 3
32sbcieg 3360 . 2
41, 3syl5bb 257 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  E.wrex 2808  [.wsbc 3327  {csn 4029
This theorem is referenced by:  rexsn  4069  rexprg  4079  rextpg  4081  iunxsng  4409  frirr  4861  frsn  5075  imasng  5364  scshwfzeqfzo  12794  mnd1  15961  mnd1OLD  15962  grp1  16142  frgra2v  24999  1vwmgra  25003  ballotlemfc0  28431  ballotlemfcc  28432  zlidlring  32734  lco0  33028  elpaddat  35528  elpadd2at  35530
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