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

Theorem ralsn 3912
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 3909 . 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 184    = wceq 1364    e. wcel 1761   A.wral 2713   _Vcvv 2970   {csn 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 962  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-ral 2718  df-v 2972  df-sbc 3184  df-sn 3875
This theorem is referenced by:  elixpsn  7298  frfi  7553  dffi3  7677  fseqenlem1  8190  fpwwe2lem13  8805  hashbc  12202  hashf1lem1  12204  cshw1  12452  rpnnen2lem11  13503  drsdirfi  15104  0subg  15699  efgsp1  16227  dprd2da  16531  lbsextlem4  17220  txkgen  19184  xkoinjcn  19219  isufil2  19440  ust0  19753  prdsxmetlem  19902  prdsbl  20025  finiunmbl  20984  xrlimcnp  22321  chtub  22510  2sqlem10  22672  dchrisum0flb  22718  pntpbnd1  22794  usgra1v  23243  constr1trl  23422  h1deoi  24887  subfacp1lem5  27002  cvmlift2lem1  27121  cvmlift2lem12  27133  heibor1lem  28633  clwwlkel  30380  bnj149  31702
  Copyright terms: Public domain W3C validator