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

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