Theorem ralsn 4634

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∀wral 3047  Vcvv 3436  {csn 4576

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-sn 4577

This theorem is referenced by:  xpord2indlem  8077  xpord3inddlem  8084  naddcllem  8591  naddasslem1  8609  naddasslem2  8610  elixpsn  8861  frfi  9169  dffi3  9315  ssttrcl  9605  ttrclss  9610  ttrclselem2  9616  fseqenlem1  9912  fpwwe2lem12  10530  hashbc  14357  hashf1lem1  14359  eqs1  14517  cshw1  14726  rpnnen2lem11  16130  drsdirfi  18208  0subg  19061  0subgOLD  19062  0subgALT  19478  efgsp1  19647  dprd2da  19954  lbsextlem4  21096  rnglidl0  21164  ply1coe  22211  mat0dimcrng  22383  txkgen  23565  xkoinjcn  23600  isufil2  23821  ust0  24133  prdsxmetlem  24281  prdsbl  24404  finiunmbl  25470  xrlimcnp  26903  chtub  27148  2sqlem10  27364  dchrisum0flb  27446  pntpbnd1  27522  conway  27738  etasslt  27752  slerec  27758  bday1s  27773  madebdaylemlrcut  27842  precsexlem9  28151  onscutlt  28199  onsiso  28203  n0sfincut  28280  bdayn0p1  28292  zscut  28329  twocut  28344  halfcut  28376  addhalfcut  28377  pw2cut2  28380  usgr1e  29221  nbgr2vtx1edg  29326  nbuhgr2vtx1edgb  29328  wlkl1loop  29614  crctcshwlkn0lem7  29792  2pthdlem1  29906  rusgrnumwwlkl1  29944  clwwlkccatlem  29964  clwwlkn2  30019  clwwlkel  30021  clwwlkwwlksb  30029  1wlkdlem4  30115  h1deoi  31524  bnj149  34882  subfacp1lem5  35216  cvmlift2lem1  35334  cvmlift2lem12  35346  lindsenlbs  37654  poimirlem28  37687  poimirlem32  37691  heibor1lem  37848  nadd1suc  43424  nregmodel  45049  usgrexmpl1lem  48051  usgrexmpl2lem  48056  isinito2lem  49529  setc1onsubc  49633