Theorem ralsn 4639

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∀wral 3075  Vcvv 3453  {csn 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-v 3455  df-sn 4582

This theorem is referenced by:  xpord2indlem  8122  xpord3inddlem  8129  naddcllem  8641  naddasslem1  8660  naddasslem2  8661  elixpsn  8915  frfi  9225  dffi3  9374  ssttrcl  9667  ttrclss  9672  ttrclselem2  9678  fseqenlem1  9977  fpwwe2lem12  10597  hashbc  14463  hashf1lem1  14465  eqs1  14623  cshw1  14832  rpnnen2lem11  16239  drsdirfi  18320  0subg  19176  0subgALT  19591  efgsp1  19760  dprd2da  20067  lbsextlem4  21211  rnglidl0  21279  ply1coe  22341  mat0dimcrng  22510  txkgen  23692  xkoinjcn  23727  isufil2  23948  ust0  24260  prdsxmetlem  24408  prdsbl  24531  finiunmbl  25586  xrlimcnp  27010  chtub  27253  2sqlem10  27469  dchrisum0flb  27551  pntpbnd1  27627  conway  27849  etaslts  27863  lesrec  27869  bday1  27884  madebdaylemlrcut  27969  precsexlem9  28285  oncutlt  28334  oniso  28341  n0fincut  28425  bdayn0p1  28439  zcuts  28477  twocut  28493  halfcut  28528  addhalfcut  28529  pw2cut2  28532  1reno  28567  usgr1e  29392  nbgr2vtx1edg  29497  nbuhgr2vtx1edgb  29499  wlkl1loop  29784  crctcshwlkn0lem7  29962  2pthdlem1  30076  rusgrnumwwlkl1  30117  clwwlkccatlem  30137  clwwlkn2  30192  clwwlkel  30194  clwwlkwwlksb  30202  1wlkdlem4  30288  h1deoi  31698  selvply1rhmlemb  33777  vieta  33838  bnj149  35134  subfacp1lem5  35498  cvmlift2lem1  35616  cvmlift2lem12  35628  lindsenlbs  38078  poimirlem28  38111  poimirlem32  38115  heibor1lem  38272  nadd1suc  43933  nregmodel  45557  usgrexmpl1lem  48607  usgrexmpl2lem  48612  isinito2lem  50083  setc1onsubc  50187