Theorem ralsn 4685

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∀wral 3058  Vcvv 3477  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-v 3479  df-sn 4631

This theorem is referenced by:  xpord2indlem  8170  xpord3inddlem  8177  naddcllem  8712  naddasslem1  8730  naddasslem2  8731  elixpsn  8975  frfi  9318  dffi3  9468  ssttrcl  9752  ttrclss  9757  ttrclselem2  9763  fseqenlem1  10061  fpwwe2lem12  10679  hashbc  14488  hashf1lem1  14490  eqs1  14646  cshw1  14856  rpnnen2lem11  16256  drsdirfi  18362  0subg  19181  0subgOLD  19182  0subgALT  19600  efgsp1  19769  dprd2da  20076  lbsextlem4  21180  rnglidl0  21256  ply1coe  22317  mat0dimcrng  22491  txkgen  23675  xkoinjcn  23710  isufil2  23931  ust0  24243  prdsxmetlem  24393  prdsbl  24519  finiunmbl  25592  xrlimcnp  27025  chtub  27270  2sqlem10  27486  dchrisum0flb  27568  pntpbnd1  27644  conway  27858  etasslt  27872  slerec  27878  bday1s  27890  madebdaylemlrcut  27951  precsexlem9  28253  zscut  28407  nohalf  28421  halfcut  28430  addhalfcut  28433  usgr1e  29276  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  wlkl1loop  29670  crctcshwlkn0lem7  29845  2pthdlem1  29959  rusgrnumwwlkl1  29997  clwwlkccatlem  30017  clwwlkn2  30072  clwwlkel  30074  clwwlkwwlksb  30082  1wlkdlem4  30168  h1deoi  31577  bnj149  34867  subfacp1lem5  35168  cvmlift2lem1  35286  cvmlift2lem12  35298  lindsenlbs  37601  poimirlem28  37634  poimirlem32  37638  heibor1lem  37795  nadd1suc  43381  usgrexmpl1lem  47915  usgrexmpl2lem  47920