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

Step	Hyp	Ref	Expression
1		rexsns 4062	. 2
2		ralsng.1	. . 3
3	2	sbcieg 3360	. 2
4	1, 3	syl5bb 257	1

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