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

Theorem ralsn 4360
Description: Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
Hypotheses
Ref Expression
ralsn.1 𝐴 ∈ V
ralsn.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ralsn (∀𝑥 ∈ {𝐴}𝜑𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ralsn
StepHypRef Expression
1 ralsn.1 . 2 𝐴 ∈ V
2 ralsn.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32ralsng 4356 . 2 (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥 ∈ {𝐴}𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wcel 2145  wral 3061  Vcvv 3351  {csn 4316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353  df-sbc 3588  df-sn 4317
This theorem is referenced by:  elixpsn  8101  frfi  8361  dffi3  8493  fseqenlem1  9047  fpwwe2lem13  9666  hashbc  13439  hashf1lem1  13441  eqs1  13592  cshw1  13777  rpnnen2lem11  15159  drsdirfi  17146  0subg  17827  efgsp1  18357  dprd2da  18649  lbsextlem4  19376  ply1coe  19881  mat0dimcrng  20494  txkgen  21676  xkoinjcn  21711  isufil2  21932  ust0  22243  prdsxmetlem  22393  prdsbl  22516  finiunmbl  23532  xrlimcnp  24916  chtub  25158  2sqlem10  25374  dchrisum0flb  25420  pntpbnd1  25496  usgr1e  26360  nbgr2vtx1edg  26469  nbuhgr2vtx1edgb  26471  wlkl1loop  26769  crctcshwlkn0lem7  26944  2pthdlem1  27077  rusgrnumwwlkl1  27117  clwwlkccatlem  27139  clwwlkn2  27200  clwwlkel  27202  clwwlkwwlksb  27211  1wlkdlem4  27320  h1deoi  28748  bnj149  31283  subfacp1lem5  31504  cvmlift2lem1  31622  cvmlift2lem12  31634  conway  32247  etasslt  32257  slerec  32260  lindsenlbs  33737  poimirlem28  33770  poimirlem32  33774  heibor1lem  33940
  Copyright terms: Public domain W3C validator