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

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
StepHypRef Expression
1 rexsns 4065 . 2  |-  ( E. x  e.  { A } ph  <->  [. A  /  x ]. ph )
2 ralsng.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3360 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3syl5bb 257 1  |-  ( A  e.  V  ->  ( E. x  e.  { A } ph  <->  ps ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator