MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralsn Structured version   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  7093  frfi  7344  dffi3  7428  fseqenlem1  7895  fpwwe2lem13  8507  hashbc  11692  hashf1lem1  11694  rpnnen2lem11  12814  drsdirfi  14385  0subg  14955  efgsp1  15359  dprd2da  15590  lbsextlem4  16223  txkgen  17674  xkoinjcn  17709  isufil2  17930  ust0  18239  prdsxmetlem  18388  prdsbl  18511  finiunmbl  19428  xrlimcnp  20797  chtub  20986  2sqlem10  21148  dchrisum0flb  21194  pntpbnd1  21270  usgra1v  21399  constr1trl  21578  h1deoi  23041  subfacp1lem5  24860  cvmlift2lem1  24979  cvmlift2lem12  24991  heibor1lem  26472  cshw1  28202  cshwssizelem1  28207  bnj149  29147
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