Theorem ralsn 4583

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2112  ∀wral 3051  Vcvv 3398  {csn 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-v 3400  df-sn 4528

This theorem is referenced by:  elixpsn  8596  frfi  8894  dffi3  9025  fseqenlem1  9603  fpwwe2lem12  10221  hashbc  13982  hashf1lem1  13985  hashf1lem1OLD  13986  eqs1  14134  cshw1  14352  rpnnen2lem11  15748  drsdirfi  17766  0subg  18522  efgsp1  19081  dprd2da  19383  lbsextlem4  20152  ply1coe  21171  mat0dimcrng  21321  txkgen  22503  xkoinjcn  22538  isufil2  22759  ust0  23071  prdsxmetlem  23220  prdsbl  23343  finiunmbl  24395  xrlimcnp  25805  chtub  26047  2sqlem10  26263  dchrisum0flb  26345  pntpbnd1  26421  usgr1e  27287  nbgr2vtx1edg  27392  nbuhgr2vtx1edgb  27394  wlkl1loop  27679  crctcshwlkn0lem7  27854  2pthdlem1  27968  rusgrnumwwlkl1  28006  clwwlkccatlem  28026  clwwlkn2  28081  clwwlkel  28083  clwwlkwwlksb  28091  1wlkdlem4  28177  h1deoi  29584  bnj149  32522  subfacp1lem5  32813  cvmlift2lem1  32931  cvmlift2lem12  32943  xpord2ind  33474  xpord3ind  33480  naddcllem  33517  conway  33679  etasslt  33693  slerec  33699  bday1s  33711  madebdaylemlrcut  33765  lindsenlbs  35458  poimirlem28  35491  poimirlem32  35495  heibor1lem  35653