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

Theorem ralsn 4169
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 4165 . 2 (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥 ∈ {𝐴}𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  wcel 1977  wral 2896  Vcvv 3173  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-sbc 3403  df-sn 4126
This theorem is referenced by:  elixpsn  7833  frfi  8090  dffi3  8220  fseqenlem1  8730  fpwwe2lem13  9343  hashbc  13094  hashf1lem1  13096  eqs1  13245  cshw1  13419  rpnnen2lem11  14792  drsdirfi  16761  0subg  17442  efgsp1  17973  dprd2da  18264  lbsextlem4  18982  ply1coe  19487  mat0dimcrng  20095  txkgen  21265  xkoinjcn  21300  isufil2  21522  ust0  21833  prdsxmetlem  21983  prdsbl  22106  finiunmbl  23119  xrlimcnp  24495  chtub  24737  2sqlem10  24953  dchrisum0flb  24999  pntpbnd1  25075  usgra1v  25919  constr1trl  26118  clwwlkel  26321  rusgranumwlkl1  26474  h1deoi  27792  bnj149  30199  subfacp1lem5  30420  cvmlift2lem1  30538  cvmlift2lem12  30550  lindsenlbs  32574  poimirlem28  32607  poimirlem32  32611  heibor1lem  32778  usgr1e  40471  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  1wlkl1loop  40842  crctcsh1wlkn0lem7  41019  2pthdlem1  41137  rusgrnumwwlkl1  41172  clwwlksn2  41217  clwwlksel  41221  11wlkdlem4  41307
  Copyright terms: Public domain W3C validator