Theorem rexsng 4068

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)

Hypothesis

Ref	Expression
ralsng.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
rexsng	|- ( A e. V -> ( E. x e. { A } ph <-> ps ) )

Distinct variable groups:   x, A   ps, x

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem rexsng

Step	Hyp	Ref	Expression
1		rexsns 4065	. 2 |- ( E. x e. { A } ph <-> [. A / x ]. ph )
2		ralsng.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	sbcieg 3360	. 2 |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
4	1, 3	syl5bb 257	1 |- ( A e. V -> ( E. x e. { A } ph <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1395   e. wcel 1819   E.wrex 2808   [.wsbc 3327   {csn 4032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-rex 2813  df-v 3111  df-sbc 3328  df-sn 4033

This theorem is referenced by:  rexsn  4072  rexprg  4082  rextpg  4084  iunxsng  4414  frirr  4865  frsn  5079  imasng  5369  scshwfzeqfzo  12806  mnd1  16088  mnd1OLD  16089  grp1  16269  frgra2v  25126  1vwmgra  25130  ballotlemfc0  28628  ballotlemfcc  28629  zlidlring  32878  lco0  33172  elpaddat  35671  elpadd2at  35673