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

Theorem ralsn 3841
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 3838 . 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 177    = wceq 1652    e. wcel 1725   A.wral 2697   _Vcvv 2948   {csn 3806
This theorem is referenced by:  elixpsn  7092  frfi  7343  dffi3  7427  fseqenlem1  7894  fpwwe2lem13  8506  hashbc  11690  hashf1lem1  11692  rpnnen2lem11  12812  drsdirfi  14383  0subg  14953  efgsp1  15357  dprd2da  15588  lbsextlem4  16221  txkgen  17672  xkoinjcn  17707  isufil2  17928  ust0  18237  prdsxmetlem  18386  prdsbl  18509  finiunmbl  19426  xrlimcnp  20795  chtub  20984  2sqlem10  21146  dchrisum0flb  21192  pntpbnd1  21268  usgra1v  21397  constr1trl  21576  h1deoi  23039  subfacp1lem5  24858  cvmlift2lem1  24977  cvmlift2lem12  24989  heibor1lem  26455  shwrdssizelem1  28166  bnj149  29100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950  df-sbc 3154  df-sn 3812
  Copyright terms: Public domain W3C validator