Theorem ralsn 4686

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ∀wral 3062  Vcvv 3475  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-sn 4630

This theorem is referenced by:  xpord2indlem  8133  xpord3inddlem  8140  naddcllem  8675  naddasslem1  8693  naddasslem2  8694  elixpsn  8931  frfi  9288  dffi3  9426  ssttrcl  9710  ttrclss  9715  ttrclselem2  9721  fseqenlem1  10019  fpwwe2lem12  10637  hashbc  14412  hashf1lem1  14415  hashf1lem1OLD  14416  eqs1  14562  cshw1  14772  rpnnen2lem11  16167  drsdirfi  18258  0subg  19031  0subgOLD  19032  0subgALT  19436  efgsp1  19605  dprd2da  19912  lbsextlem4  20774  ply1coe  21820  mat0dimcrng  21972  txkgen  23156  xkoinjcn  23191  isufil2  23412  ust0  23724  prdsxmetlem  23874  prdsbl  24000  finiunmbl  25061  xrlimcnp  26473  chtub  26715  2sqlem10  26931  dchrisum0flb  27013  pntpbnd1  27089  conway  27300  etasslt  27314  slerec  27320  bday1s  27332  madebdaylemlrcut  27393  precsexlem9  27661  usgr1e  28502  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  wlkl1loop  28895  crctcshwlkn0lem7  29070  2pthdlem1  29184  rusgrnumwwlkl1  29222  clwwlkccatlem  29242  clwwlkn2  29297  clwwlkel  29299  clwwlkwwlksb  29307  1wlkdlem4  29393  h1deoi  30802  bnj149  33886  subfacp1lem5  34175  cvmlift2lem1  34293  cvmlift2lem12  34305  lindsenlbs  36483  poimirlem28  36516  poimirlem32  36520  heibor1lem  36677  nadd1suc  42142  rnglidl0  46752