Theorem ralsn 4625

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3051  Vcvv 3429  {csn 4567

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-sn 4568

This theorem is referenced by:  xpord2indlem  8097  xpord3inddlem  8104  naddcllem  8612  naddasslem1  8630  naddasslem2  8631  elixpsn  8885  frfi  9195  dffi3  9344  ssttrcl  9636  ttrclss  9641  ttrclselem2  9647  fseqenlem1  9946  fpwwe2lem12  10565  hashbc  14415  hashf1lem1  14417  eqs1  14575  cshw1  14784  rpnnen2lem11  16191  drsdirfi  18271  0subg  19127  0subgALT  19543  efgsp1  19712  dprd2da  20019  lbsextlem4  21159  rnglidl0  21227  ply1coe  22263  mat0dimcrng  22435  txkgen  23617  xkoinjcn  23652  isufil2  23873  ust0  24185  prdsxmetlem  24333  prdsbl  24456  finiunmbl  25511  xrlimcnp  26932  chtub  27175  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  conway  27771  etaslts  27785  lesrec  27791  bday1  27806  madebdaylemlrcut  27891  precsexlem9  28207  oncutlt  28256  oniso  28263  n0fincut  28347  bdayn0p1  28361  zcuts  28399  twocut  28415  halfcut  28450  addhalfcut  28451  pw2cut2  28454  1reno  28489  usgr1e  29314  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  wlkl1loop  29706  crctcshwlkn0lem7  29884  2pthdlem1  29998  rusgrnumwwlkl1  30039  clwwlkccatlem  30059  clwwlkn2  30114  clwwlkel  30116  clwwlkwwlksb  30124  1wlkdlem4  30210  h1deoi  31620  vieta  33724  bnj149  35017  subfacp1lem5  35366  cvmlift2lem1  35484  cvmlift2lem12  35496  lindsenlbs  37936  poimirlem28  37969  poimirlem32  37973  heibor1lem  38130  nadd1suc  43820  nregmodel  45444  usgrexmpl1lem  48497  usgrexmpl2lem  48502  isinito2lem  49973  setc1onsubc  50077