Theorem ralsn 4617

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  ∀wral 3064  Vcvv 3429  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3431  df-sn 4562

This theorem is referenced by:  elixpsn  8712  frfi  9046  dffi3  9177  ssttrcl  9460  ttrclss  9465  ttrclselem2  9471  fseqenlem1  9790  fpwwe2lem12  10408  hashbc  14175  hashf1lem1  14178  hashf1lem1OLD  14179  eqs1  14327  cshw1  14545  rpnnen2lem11  15943  drsdirfi  18033  0subg  18790  efgsp1  19353  dprd2da  19655  lbsextlem4  20433  ply1coe  21477  mat0dimcrng  21629  txkgen  22813  xkoinjcn  22848  isufil2  23069  ust0  23381  prdsxmetlem  23531  prdsbl  23657  finiunmbl  24718  xrlimcnp  26128  chtub  26370  2sqlem10  26586  dchrisum0flb  26668  pntpbnd1  26744  usgr1e  27622  nbgr2vtx1edg  27727  nbuhgr2vtx1edgb  27729  wlkl1loop  28014  crctcshwlkn0lem7  28189  2pthdlem1  28303  rusgrnumwwlkl1  28341  clwwlkccatlem  28361  clwwlkn2  28416  clwwlkel  28418  clwwlkwwlksb  28426  1wlkdlem4  28512  h1deoi  29919  bnj149  32863  subfacp1lem5  33154  cvmlift2lem1  33272  cvmlift2lem12  33284  xpord2ind  33802  xpord3ind  33808  naddcllem  33839  conway  34001  etasslt  34015  slerec  34021  bday1s  34033  madebdaylemlrcut  34087  lindsenlbs  35780  poimirlem28  35813  poimirlem32  35817  heibor1lem  35975