Theorem ralsn 4643

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  ∀wral 3079  Vcvv 3457  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-v 3459  df-sn 4586

This theorem is referenced by:  xpord2indlem  8131  xpord3inddlem  8138  naddcllem  8650  naddasslem1  8669  naddasslem2  8670  elixpsn  8923  frfi  9233  dffi3  9379  ssttrcl  9672  ttrclss  9677  ttrclselem2  9683  fseqenlem1  9996  fpwwe2lem12  10615  hashbc  14480  hashf1lem1  14482  eqs1  14640  cshw1  14849  rpnnen2lem11  16270  drsdirfi  18351  0subg  19209  0subgALT  19629  efgsp1  19798  dprd2da  20105  lbsextlem4  21254  rnglidl0  21324  ply1coe  22419  mat0dimcrng  22588  txkgen  23770  xkoinjcn  23805  isufil2  24026  ust0  24338  prdsxmetlem  24486  prdsbl  24609  finiunmbl  25664  xrlimcnp  27091  chtub  27334  2sqlem10  27550  dchrisum0flb  27632  pntpbnd1  27708  conway  27930  etaslts  27944  lesrec  27950  bday1  27965  madebdaylemlrcut  28050  precsexlem9  28366  oncutlt  28415  oniso  28422  n0fincut  28506  bdayn0p1  28520  zcuts  28558  twocut  28574  halfcut  28609  addhalfcut  28610  pw2cut2  28613  1reno  28648  usgr1e  29504  nbgr2vtx1edg  29609  nbuhgr2vtx1edgb  29611  wlkl1loop  29896  crctcshwlkn0lem7  30074  2pthdlem1  30188  rusgrnumwwlkl1  30229  clwwlkccatlem  30249  clwwlkn2  30304  clwwlkel  30306  clwwlkwwlksb  30314  1wlkdlem4  30400  h1deoi  31810  selvply1rhmlemb  33826  vieta  33887  bnj149  35180  subfacp1lem5  35547  cvmlift2lem1  35665  cvmlift2lem12  35677  lindsenlbs  38126  poimirlem28  38159  poimirlem32  38163  heibor1lem  38320  nadd1suc  43981  nregmodel  45591  usgrexmpl1lem  48641  usgrexmpl2lem  48646  isinito2lem  50127  setc1onsubc  50231