Theorem ralsn 4620

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 4614	. 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∀wral 3054  Vcvv 3432  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-v 3434  df-sn 4563

This theorem is referenced by:  xpord2indlem  8094  xpord3inddlem  8101  naddcllem  8609  naddasslem1  8627  naddasslem2  8628  elixpsn  8882  frfi  9192  dffi3  9341  ssttrcl  9634  ttrclss  9639  ttrclselem2  9645  fseqenlem1  9944  fpwwe2lem12  10563  hashbc  14413  hashf1lem1  14415  eqs1  14573  cshw1  14782  rpnnen2lem11  16189  drsdirfi  18269  0subg  19125  0subgALT  19541  efgsp1  19710  dprd2da  20017  lbsextlem4  21161  rnglidl0  21229  ply1coe  22291  mat0dimcrng  22460  txkgen  23642  xkoinjcn  23677  isufil2  23898  ust0  24210  prdsxmetlem  24358  prdsbl  24481  finiunmbl  25536  xrlimcnp  26957  chtub  27200  2sqlem10  27416  dchrisum0flb  27498  pntpbnd1  27574  conway  27796  etaslts  27810  lesrec  27816  bday1  27831  madebdaylemlrcut  27916  precsexlem9  28232  oncutlt  28281  oniso  28288  n0fincut  28372  bdayn0p1  28386  zcuts  28424  twocut  28440  halfcut  28475  addhalfcut  28476  pw2cut2  28479  1reno  28514  usgr1e  29339  nbgr2vtx1edg  29444  nbuhgr2vtx1edgb  29446  wlkl1loop  29731  crctcshwlkn0lem7  29909  2pthdlem1  30023  rusgrnumwwlkl1  30064  clwwlkccatlem  30084  clwwlkn2  30139  clwwlkel  30141  clwwlkwwlksb  30149  1wlkdlem4  30235  h1deoi  31645  selvply1rhmlemb  33710  vieta  33771  bnj149  35064  subfacp1lem5  35419  cvmlift2lem1  35537  cvmlift2lem12  35549  lindsenlbs  37989  poimirlem28  38022  poimirlem32  38026  heibor1lem  38183  nadd1suc  43844  nregmodel  45468  usgrexmpl1lem  48519  usgrexmpl2lem  48524  isinito2lem  49995  setc1onsubc  50099