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

Theorem ralsn 4013
Description: Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
Hypotheses
Ref Expression
ralsn.1  |-  A  e. 
_V
ralsn.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ralsn  |-  ( A. x  e.  { A } ph  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem ralsn
StepHypRef Expression
1 ralsn.1 . 2  |-  A  e. 
_V
2 ralsn.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32ralsng 4009 . 2  |-  ( A  e.  _V  ->  ( A. x  e.  { A } ph  <->  ps ) )
41, 3ax-mp 5 1  |-  ( A. x  e.  { A } ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    = wceq 1407    e. wcel 1844   A.wral 2756   _Vcvv 3061   {csn 3974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-ral 2761  df-v 3063  df-sbc 3280  df-sn 3975
This theorem is referenced by:  elixpsn  7548  frfi  7801  dffi3  7927  fseqenlem1  8439  fpwwe2lem13  9052  hashbc  12553  hashf1lem1  12555  eqs1  12677  cshw1  12848  rpnnen2lem11  14169  drsdirfi  15893  0subg  16552  efgsp1  17081  dprd2da  17413  lbsextlem4  18129  ply1coe  18659  mat0dimcrng  19266  txkgen  20447  xkoinjcn  20482  isufil2  20703  ust0  21016  prdsxmetlem  21165  prdsbl  21288  finiunmbl  22248  xrlimcnp  23626  chtub  23870  2sqlem10  24032  dchrisum0flb  24078  pntpbnd1  24154  usgra1v  24819  constr1trl  25019  clwwlkel  25222  rusgranumwlkl1  25376  h1deoi  26894  bnj149  29273  subfacp1lem5  29494  cvmlift2lem1  29612  cvmlift2lem12  29624  heibor1lem  31600
  Copyright terms: Public domain W3C validator