Theorem ralsn 4626

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

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

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 3432  df-sn 4569

This theorem is referenced by:  xpord2indlem  8090  xpord3inddlem  8097  naddcllem  8605  naddasslem1  8623  naddasslem2  8624  elixpsn  8878  frfi  9188  dffi3  9337  ssttrcl  9627  ttrclss  9632  ttrclselem2  9638  fseqenlem1  9937  fpwwe2lem12  10556  hashbc  14406  hashf1lem1  14408  eqs1  14566  cshw1  14775  rpnnen2lem11  16182  drsdirfi  18262  0subg  19118  0subgALT  19534  efgsp1  19703  dprd2da  20010  lbsextlem4  21151  rnglidl0  21219  ply1coe  22273  mat0dimcrng  22445  txkgen  23627  xkoinjcn  23662  isufil2  23883  ust0  24195  prdsxmetlem  24343  prdsbl  24466  finiunmbl  25521  xrlimcnp  26945  chtub  27189  2sqlem10  27405  dchrisum0flb  27487  pntpbnd1  27563  conway  27785  etaslts  27799  lesrec  27805  bday1  27820  madebdaylemlrcut  27905  precsexlem9  28221  oncutlt  28270  oniso  28277  n0fincut  28361  bdayn0p1  28375  zcuts  28413  twocut  28429  halfcut  28464  addhalfcut  28465  pw2cut2  28468  1reno  28503  usgr1e  29328  nbgr2vtx1edg  29433  nbuhgr2vtx1edgb  29435  wlkl1loop  29721  crctcshwlkn0lem7  29899  2pthdlem1  30013  rusgrnumwwlkl1  30054  clwwlkccatlem  30074  clwwlkn2  30129  clwwlkel  30131  clwwlkwwlksb  30139  1wlkdlem4  30225  h1deoi  31635  vieta  33739  bnj149  35033  subfacp1lem5  35382  cvmlift2lem1  35500  cvmlift2lem12  35512  lindsenlbs  37950  poimirlem28  37983  poimirlem32  37987  heibor1lem  38144  nadd1suc  43838  nregmodel  45462  usgrexmpl1lem  48509  usgrexmpl2lem  48514  isinito2lem  49985  setc1onsubc  50089