Theorem ralsn 4645

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3447  {csn 4589

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-sn 4590

This theorem is referenced by:  xpord2indlem  8126  xpord3inddlem  8133  naddcllem  8640  naddasslem1  8658  naddasslem2  8659  elixpsn  8910  frfi  9232  dffi3  9382  ssttrcl  9668  ttrclss  9673  ttrclselem2  9679  fseqenlem1  9977  fpwwe2lem12  10595  hashbc  14418  hashf1lem1  14420  eqs1  14577  cshw1  14787  rpnnen2lem11  16192  drsdirfi  18266  0subg  19083  0subgOLD  19084  0subgALT  19498  efgsp1  19667  dprd2da  19974  lbsextlem4  21071  rnglidl0  21139  ply1coe  22185  mat0dimcrng  22357  txkgen  23539  xkoinjcn  23574  isufil2  23795  ust0  24107  prdsxmetlem  24256  prdsbl  24379  finiunmbl  25445  xrlimcnp  26878  chtub  27123  2sqlem10  27339  dchrisum0flb  27421  pntpbnd1  27497  conway  27711  etasslt  27725  slerec  27731  bday1s  27743  madebdaylemlrcut  27810  precsexlem9  28117  onscutlt  28165  onsiso  28169  n0sfincut  28246  bdayn0p1  28258  zscut  28295  twocut  28309  halfcut  28333  addhalfcut  28334  usgr1e  29172  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  wlkl1loop  29566  crctcshwlkn0lem7  29746  2pthdlem1  29860  rusgrnumwwlkl1  29898  clwwlkccatlem  29918  clwwlkn2  29973  clwwlkel  29975  clwwlkwwlksb  29983  1wlkdlem4  30069  h1deoi  31478  bnj149  34865  subfacp1lem5  35171  cvmlift2lem1  35289  cvmlift2lem12  35301  lindsenlbs  37609  poimirlem28  37642  poimirlem32  37646  heibor1lem  37803  nadd1suc  43381  nregmodel  45007  usgrexmpl1lem  48012  usgrexmpl2lem  48017  isinito2lem  49487  setc1onsubc  49591