Theorem ralsn 4640

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3442  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-sn 4583

This theorem is referenced by:  xpord2indlem  8099  xpord3inddlem  8106  naddcllem  8614  naddasslem1  8632  naddasslem2  8633  elixpsn  8887  frfi  9197  dffi3  9346  ssttrcl  9636  ttrclss  9641  ttrclselem2  9647  fseqenlem1  9946  fpwwe2lem12  10565  hashbc  14388  hashf1lem1  14390  eqs1  14548  cshw1  14757  rpnnen2lem11  16161  drsdirfi  18240  0subg  19093  0subgALT  19509  efgsp1  19678  dprd2da  19985  lbsextlem4  21128  rnglidl0  21196  ply1coe  22254  mat0dimcrng  22426  txkgen  23608  xkoinjcn  23643  isufil2  23864  ust0  24176  prdsxmetlem  24324  prdsbl  24447  finiunmbl  25513  xrlimcnp  26946  chtub  27191  2sqlem10  27407  dchrisum0flb  27489  pntpbnd1  27565  conway  27787  etaslts  27801  lesrec  27807  bday1  27822  madebdaylemlrcut  27907  precsexlem9  28223  oncutlt  28272  oniso  28279  n0fincut  28363  bdayn0p1  28377  zcuts  28415  twocut  28431  halfcut  28466  addhalfcut  28467  pw2cut2  28470  1reno  28505  usgr1e  29330  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  wlkl1loop  29723  crctcshwlkn0lem7  29901  2pthdlem1  30015  rusgrnumwwlkl1  30056  clwwlkccatlem  30076  clwwlkn2  30131  clwwlkel  30133  clwwlkwwlksb  30141  1wlkdlem4  30227  h1deoi  31636  vieta  33756  bnj149  35050  subfacp1lem5  35397  cvmlift2lem1  35515  cvmlift2lem12  35527  lindsenlbs  37860  poimirlem28  37893  poimirlem32  37897  heibor1lem  38054  nadd1suc  43743  nregmodel  45367  usgrexmpl1lem  48375  usgrexmpl2lem  48380  isinito2lem  49851  setc1onsubc  49955