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

Theorem ralsn 4198
 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 4194 . 2 (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥 ∈ {𝐴}𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ∈ wcel 1987  ∀wral 2907  Vcvv 3189  {csn 4153 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-v 3191  df-sbc 3422  df-sn 4154 This theorem is referenced by:  elixpsn  7899  frfi  8157  dffi3  8289  fseqenlem1  8799  fpwwe2lem13  9416  hashbc  13183  hashf1lem1  13185  eqs1  13339  cshw1  13513  rpnnen2lem11  14889  drsdirfi  16870  0subg  17551  efgsp1  18082  dprd2da  18373  lbsextlem4  19093  ply1coe  19598  mat0dimcrng  20208  txkgen  21378  xkoinjcn  21413  isufil2  21635  ust0  21946  prdsxmetlem  22096  prdsbl  22219  finiunmbl  23235  xrlimcnp  24612  chtub  24854  2sqlem10  25070  dchrisum0flb  25116  pntpbnd1  25192  usgr1e  26047  nbgr2vtx1edg  26150  nbuhgr2vtx1edgb  26152  wlkl1loop  26420  crctcshwlkn0lem7  26594  2pthdlem1  26712  rusgrnumwwlkl1  26747  clwwlksn2  26793  clwwlksel  26797  1wlkdlem4  26883  h1deoi  28278  bnj149  30688  subfacp1lem5  30909  cvmlift2lem1  31027  cvmlift2lem12  31039  lindsenlbs  33071  poimirlem28  33104  poimirlem32  33108  heibor1lem  33275
 Copyright terms: Public domain W3C validator