Theorem rexsng 4056

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 4053	. 2 |- ( E. x e. { A } ph <-> [. A / x ]. ph )
2		ralsng.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	sbcieg 3357	. 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 1374   e. wcel 1762   E.wrex 2808   [.wsbc 3324   {csn 4020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-rex 2813  df-v 3108  df-sbc 3325  df-sn 4021

This theorem is referenced by:  rexsn  4060  rexprg  4070  rextpg  4072  iunxsng  4397  frirr  4849  frsn  5062  imasng  5350  scshwfzeqfzo  12744  frgra2v  24661  1vwmgra  24665  ballotlemfc0  28057  ballotlemfcc  28058  lco0  31976  mnd1  32036  grp1  32037  elpaddat  34475  elpadd2at  34477