Theorem ralsn 4642

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ∀wral 3080  Vcvv 3454  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-sn 4589

This theorem is used by:  xpord2indlem  8191  xpord3inddlem  8198  naddcllem  8713  naddasslem1  8732  naddasslem2  8733  elixpsn  8993  frfi  9304  dffi3  9450  ssttrcl  9743  ttrclss  9748  ttrclselem2  9754  fseqenlem1  10130  fpwwe2lem12  10754  hashbc  14625  hashf1lem1  14627  eqs1  14788  cshw1  15001  rpnnen2lem11  16421  drsdirfi  18508  0subg  19391  0subgALT  19812  efgsp1  19981  dprd2da  20288  lbsextlem4  21469  rnglidl0  21539  lindsenlbs  22187  ply1coe  22646  mat0dimcrng  22815  txkgen  24001  xkoinjcn  24036  isufil2  24257  ust0  24569  prdsxmetlem  24717  prdsbl  24840  finiunmbl  25895  xrlimcnp  27326  chtub  27569  2sqlem10  27785  dchrisum0flb  27867  pntpbnd1  27943  conway  28195  etaslts  28209  lesrec  28215  bday1  28230  madebdaylemlrcut  28315  precsexlem9  28631  oncutlt  28680  oniso  28687  n0fincut  28771  bdayn0p1  28785  zcuts  28823  twocut  28839  halfcut  28874  addhalfcut  28875  pw2cut2  28878  1reno  28913  usgr1e  29856  nbgr2vtx1edg  29961  nbuhgr2vtx1edgb  29963  wlkl1loop  30248  crctcshwlkn0lem7  30435  2pthdlem1  30549  rusgrnumwwlkl1  30590  clwwlkccatlem  30610  clwwlkn2  30665  clwwlkel  30667  clwwlkwwlksb  30675  1wlkdlem4  30761  h1deoi  32181  selvply1rhmlemb  34221  vieta  34282  bnj149  35575  subfacp1lem5  36116  cvmlift2lem1  36234  cvmlift2lem12  36246  nmulrid  37124  poimirlem28  38758  poimirlem32  38762  heibor1lem  38935  nadd1suc  44586  nregmodel  46202  usgrexmpl1lem  49324  usgrexmpl2lem  49329  isinito2lem  50838  setc1onsubc  50945