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

Theorem ralsn 4013
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 4010 . 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 1370    e. wcel 1758   A.wral 2795   _Vcvv 3068   {csn 3975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-ral 2800  df-v 3070  df-sbc 3285  df-sn 3976
This theorem is referenced by:  elixpsn  7402  frfi  7658  dffi3  7782  fseqenlem1  8295  fpwwe2lem13  8910  hashbc  12308  hashf1lem1  12310  cshw1  12558  rpnnen2lem11  13609  drsdirfi  15210  0subg  15808  efgsp1  16338  dprd2da  16646  lbsextlem4  17348  ply1coe  17855  txkgen  19341  xkoinjcn  19376  isufil2  19597  ust0  19910  prdsxmetlem  20059  prdsbl  20182  finiunmbl  21141  xrlimcnp  22478  chtub  22667  2sqlem10  22829  dchrisum0flb  22875  pntpbnd1  22951  usgra1v  23443  constr1trl  23622  h1deoi  25087  subfacp1lem5  27206  cvmlift2lem1  27325  cvmlift2lem12  27337  heibor1lem  28846  clwwlkel  30593  bnj149  32168
  Copyright terms: Public domain W3C validator