Theorem rexsng 4013

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 4010	. 2 |- ( E. x e. { A } ph <-> [. A / x ]. ph )
2		ralsng.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	sbcieg 3319	. 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 1370   e. wcel 1758   E.wrex 2796   [.wsbc 3286   {csn 3977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-rex 2801  df-v 3072  df-sbc 3287  df-sn 3978

This theorem is referenced by:  rexsn  4016  rexprg  4026  rextpg  4028  iunxsng  4349  frirr  4797  frsn  5009  imasng  5291  ballotlemfc0  27011  ballotlemfcc  27012  scshwfzeqfzo  30632  frgra2v  30731  1vwmgra  30735  lco0  31070  mnd1  31130  grp1  31131  elpaddat  33756  elpadd2at  33758