Theorem ralsn 4657

Description: Convert a universal quantification restricted to 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

Step	Hyp	Ref	Expression
1		ralsn.1	. 2 ⊢ 𝐴 ∈ V
2		ralsn.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	ralsng 4651	. 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3051  Vcvv 3459  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-sn 4602

This theorem is referenced by:  xpord2indlem  8146  xpord3inddlem  8153  naddcllem  8688  naddasslem1  8706  naddasslem2  8707  elixpsn  8951  frfi  9293  dffi3  9443  ssttrcl  9729  ttrclss  9734  ttrclselem2  9740  fseqenlem1  10038  fpwwe2lem12  10656  hashbc  14471  hashf1lem1  14473  eqs1  14630  cshw1  14840  rpnnen2lem11  16242  drsdirfi  18317  0subg  19134  0subgOLD  19135  0subgALT  19549  efgsp1  19718  dprd2da  20025  lbsextlem4  21122  rnglidl0  21190  ply1coe  22236  mat0dimcrng  22408  txkgen  23590  xkoinjcn  23625  isufil2  23846  ust0  24158  prdsxmetlem  24307  prdsbl  24430  finiunmbl  25497  xrlimcnp  26930  chtub  27175  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  conway  27763  etasslt  27777  slerec  27783  bday1s  27795  madebdaylemlrcut  27862  precsexlem9  28169  onscutlt  28217  onsiso  28221  n0sfincut  28298  bdayn0p1  28310  zscut  28347  twocut  28361  halfcut  28385  addhalfcut  28386  usgr1e  29224  nbgr2vtx1edg  29329  nbuhgr2vtx1edgb  29331  wlkl1loop  29618  crctcshwlkn0lem7  29798  2pthdlem1  29912  rusgrnumwwlkl1  29950  clwwlkccatlem  29970  clwwlkn2  30025  clwwlkel  30027  clwwlkwwlksb  30035  1wlkdlem4  30121  h1deoi  31530  bnj149  34906  subfacp1lem5  35206  cvmlift2lem1  35324  cvmlift2lem12  35336  lindsenlbs  37639  poimirlem28  37672  poimirlem32  37676  heibor1lem  37833  nadd1suc  43416  usgrexmpl1lem  48025  usgrexmpl2lem  48030  isinito2lem  49383  setc1onsubc  49479