Theorem ralsn 4681

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-sn 4627

This theorem is referenced by:  xpord2indlem  8172  xpord3inddlem  8179  naddcllem  8714  naddasslem1  8732  naddasslem2  8733  elixpsn  8977  frfi  9321  dffi3  9471  ssttrcl  9755  ttrclss  9760  ttrclselem2  9766  fseqenlem1  10064  fpwwe2lem12  10682  hashbc  14492  hashf1lem1  14494  eqs1  14650  cshw1  14860  rpnnen2lem11  16260  drsdirfi  18351  0subg  19169  0subgOLD  19170  0subgALT  19586  efgsp1  19755  dprd2da  20062  lbsextlem4  21163  rnglidl0  21239  ply1coe  22302  mat0dimcrng  22476  txkgen  23660  xkoinjcn  23695  isufil2  23916  ust0  24228  prdsxmetlem  24378  prdsbl  24504  finiunmbl  25579  xrlimcnp  27011  chtub  27256  2sqlem10  27472  dchrisum0flb  27554  pntpbnd1  27630  conway  27844  etasslt  27858  slerec  27864  bday1s  27876  madebdaylemlrcut  27937  precsexlem9  28239  zscut  28393  nohalf  28407  halfcut  28416  addhalfcut  28419  usgr1e  29262  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  wlkl1loop  29656  crctcshwlkn0lem7  29836  2pthdlem1  29950  rusgrnumwwlkl1  29988  clwwlkccatlem  30008  clwwlkn2  30063  clwwlkel  30065  clwwlkwwlksb  30073  1wlkdlem4  30159  h1deoi  31568  bnj149  34889  subfacp1lem5  35189  cvmlift2lem1  35307  cvmlift2lem12  35319  lindsenlbs  37622  poimirlem28  37655  poimirlem32  37659  heibor1lem  37816  nadd1suc  43405  usgrexmpl1lem  47980  usgrexmpl2lem  47985