Theorem ralsn 4661

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  ∀wral 3050  Vcvv 3463  {csn 4606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-v 3465  df-sn 4607

This theorem is referenced by:  xpord2indlem  8154  xpord3inddlem  8161  naddcllem  8696  naddasslem1  8714  naddasslem2  8715  elixpsn  8959  frfi  9303  dffi3  9453  ssttrcl  9737  ttrclss  9742  ttrclselem2  9748  fseqenlem1  10046  fpwwe2lem12  10664  hashbc  14474  hashf1lem1  14476  eqs1  14632  cshw1  14842  rpnnen2lem11  16242  drsdirfi  18321  0subg  19138  0subgOLD  19139  0subgALT  19554  efgsp1  19723  dprd2da  20030  lbsextlem4  21131  rnglidl0  21201  ply1coe  22250  mat0dimcrng  22424  txkgen  23606  xkoinjcn  23641  isufil2  23862  ust0  24174  prdsxmetlem  24323  prdsbl  24448  finiunmbl  25515  xrlimcnp  26947  chtub  27192  2sqlem10  27408  dchrisum0flb  27490  pntpbnd1  27566  conway  27780  etasslt  27794  slerec  27800  bday1s  27812  madebdaylemlrcut  27873  precsexlem9  28175  zscut  28329  nohalf  28343  halfcut  28352  addhalfcut  28355  usgr1e  29190  nbgr2vtx1edg  29295  nbuhgr2vtx1edgb  29297  wlkl1loop  29584  crctcshwlkn0lem7  29764  2pthdlem1  29878  rusgrnumwwlkl1  29916  clwwlkccatlem  29936  clwwlkn2  29991  clwwlkel  29993  clwwlkwwlksb  30001  1wlkdlem4  30087  h1deoi  31496  bnj149  34848  subfacp1lem5  35148  cvmlift2lem1  35266  cvmlift2lem12  35278  lindsenlbs  37581  poimirlem28  37614  poimirlem32  37618  heibor1lem  37775  nadd1suc  43367  usgrexmpl1lem  47938  usgrexmpl2lem  47943