Theorem ralsn 4633

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3048  Vcvv 3437  {csn 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-v 3439  df-sn 4576

This theorem is referenced by:  xpord2indlem  8083  xpord3inddlem  8090  naddcllem  8597  naddasslem1  8615  naddasslem2  8616  elixpsn  8867  frfi  9176  dffi3  9322  ssttrcl  9612  ttrclss  9617  ttrclselem2  9623  fseqenlem1  9922  fpwwe2lem12  10540  hashbc  14362  hashf1lem1  14364  eqs1  14522  cshw1  14731  rpnnen2lem11  16135  drsdirfi  18213  0subg  19066  0subgALT  19482  efgsp1  19651  dprd2da  19958  lbsextlem4  21100  rnglidl0  21168  ply1coe  22214  mat0dimcrng  22386  txkgen  23568  xkoinjcn  23603  isufil2  23824  ust0  24136  prdsxmetlem  24284  prdsbl  24407  finiunmbl  25473  xrlimcnp  26906  chtub  27151  2sqlem10  27367  dchrisum0flb  27449  pntpbnd1  27525  conway  27741  etasslt  27755  slerec  27761  bday1s  27776  madebdaylemlrcut  27845  precsexlem9  28154  onscutlt  28202  onsiso  28206  n0sfincut  28283  bdayn0p1  28295  zscut  28332  twocut  28347  halfcut  28379  addhalfcut  28380  pw2cut2  28383  usgr1e  29225  nbgr2vtx1edg  29330  nbuhgr2vtx1edgb  29332  wlkl1loop  29618  crctcshwlkn0lem7  29796  2pthdlem1  29910  rusgrnumwwlkl1  29951  clwwlkccatlem  29971  clwwlkn2  30026  clwwlkel  30028  clwwlkwwlksb  30036  1wlkdlem4  30122  h1deoi  31531  bnj149  34908  subfacp1lem5  35249  cvmlift2lem1  35367  cvmlift2lem12  35379  lindsenlbs  37675  poimirlem28  37708  poimirlem32  37712  heibor1lem  37869  nadd1suc  43509  nregmodel  45134  usgrexmpl1lem  48145  usgrexmpl2lem  48150  isinito2lem  49623  setc1onsubc  49727