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

Theorem rexsng 3784
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 3782 . 2  |-  ( A  e.  V  ->  ( E. x  e.  { A } ph  <->  [. A  /  x ]. ph ) )
2 ralsng.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3130 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3bitrd 245 1  |-  ( A  e.  V  ->  ( E. x  e.  { A } ph  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   E.wrex 2644   [.wsbc 3098   {csn 3751
This theorem is referenced by:  rexsn  3787  rexprg  3795  rextpg  3797  iunxsng  4104  frirr  4494  frsn  4882  imasng  5160  ballotlemfc0  24523  ballotlemfcc  24524  frgra2v  27746  1vwmgra  27750  elpaddat  29970  elpadd2at  29972
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-rex 2649  df-v 2895  df-sbc 3099  df-sn 3757
  Copyright terms: Public domain W3C validator