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

Theorem ralsn 3687
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 3685 . 2  |-  ( A  e.  _V  ->  ( A. x  e.  { A } ph  <->  ps ) )
41, 3ax-mp 8 1  |-  ( A. x  e.  { A } ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   A.wral 2556   _Vcvv 2801   {csn 3653
This theorem is referenced by:  elixpsn  6871  frfi  7118  dffi3  7200  fseqenlem1  7667  fpwwe2lem13  8280  hashbc  11407  hashf1lem1  11409  rpnnen2lem11  12519  drsdirfi  14088  0subg  14658  efgsp1  15062  dprd2da  15293  lbsextlem4  15930  txkgen  17362  xkoinjcn  17397  isufil2  17619  prdsxmetlem  17948  prdsbl  18053  finiunmbl  18917  xrlimcnp  20279  chtub  20467  2sqlem10  20629  dchrisum0flb  20675  pntpbnd1  20751  h1deoi  22144  subfacp1lem5  23730  cvmlift2lem1  23848  cvmlift2lem12  23860  basexre  25625  heibor1lem  26636  usgra1v  28260  bnj149  29223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-sbc 3005  df-sn 3659
  Copyright terms: Public domain W3C validator