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

Theorem ralsn 4061
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 4057 . 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 1374    e. wcel 1762   A.wral 2809   _Vcvv 3108   {csn 4022
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 1714  ax-7 1734  ax-10 1781  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-ral 2814  df-v 3110  df-sbc 3327  df-sn 4023
This theorem is referenced by:  elixpsn  7500  frfi  7756  dffi3  7882  fseqenlem1  8396  fpwwe2lem13  9011  hashbc  12457  hashf1lem1  12459  cshw1  12742  rpnnen2lem11  13810  drsdirfi  15416  0subg  16016  efgsp1  16546  dprd2da  16876  lbsextlem4  17585  ply1coe  18103  txkgen  19883  xkoinjcn  19918  isufil2  20139  ust0  20452  prdsxmetlem  20601  prdsbl  20724  finiunmbl  21684  xrlimcnp  23021  chtub  23210  2sqlem10  23372  dchrisum0flb  23418  pntpbnd1  23494  usgra1v  24054  constr1trl  24254  clwwlkel  24457  h1deoi  26131  subfacp1lem5  28256  cvmlift2lem1  28375  cvmlift2lem12  28387  heibor1lem  29897  bnj149  32889
  Copyright terms: Public domain W3C validator