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

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
StepHypRef Expression
1 rexsns 4010 . 2  |-  ( E. x  e.  { A } ph  <->  [. A  /  x ]. ph )
2 ralsng.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3319 . 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 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
  Copyright terms: Public domain W3C validator