Theorem ralsn 4638

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3051  Vcvv 3440  {csn 4580

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-sn 4581

This theorem is referenced by:  xpord2indlem  8089  xpord3inddlem  8096  naddcllem  8604  naddasslem1  8622  naddasslem2  8623  elixpsn  8875  frfi  9185  dffi3  9334  ssttrcl  9624  ttrclss  9629  ttrclselem2  9635  fseqenlem1  9934  fpwwe2lem12  10553  hashbc  14376  hashf1lem1  14378  eqs1  14536  cshw1  14745  rpnnen2lem11  16149  drsdirfi  18228  0subg  19081  0subgALT  19497  efgsp1  19666  dprd2da  19973  lbsextlem4  21116  rnglidl0  21184  ply1coe  22242  mat0dimcrng  22414  txkgen  23596  xkoinjcn  23631  isufil2  23852  ust0  24164  prdsxmetlem  24312  prdsbl  24435  finiunmbl  25501  xrlimcnp  26934  chtub  27179  2sqlem10  27395  dchrisum0flb  27477  pntpbnd1  27553  conway  27775  etaslts  27789  lesrec  27795  bday1  27810  madebdaylemlrcut  27895  precsexlem9  28211  oncutlt  28260  oniso  28267  n0fincut  28351  bdayn0p1  28365  zcuts  28403  twocut  28419  halfcut  28454  addhalfcut  28455  pw2cut2  28458  1reno  28493  usgr1e  29318  nbgr2vtx1edg  29423  nbuhgr2vtx1edgb  29425  wlkl1loop  29711  crctcshwlkn0lem7  29889  2pthdlem1  30003  rusgrnumwwlkl1  30044  clwwlkccatlem  30064  clwwlkn2  30119  clwwlkel  30121  clwwlkwwlksb  30129  1wlkdlem4  30215  h1deoi  31624  vieta  33736  bnj149  35031  subfacp1lem5  35378  cvmlift2lem1  35496  cvmlift2lem12  35508  lindsenlbs  37812  poimirlem28  37845  poimirlem32  37849  heibor1lem  38006  nadd1suc  43630  nregmodel  45254  usgrexmpl1lem  48263  usgrexmpl2lem  48268  isinito2lem  49739  setc1onsubc  49843