Theorem ralsn 4635

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3438  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-sn 4580

This theorem is referenced by:  xpord2indlem  8087  xpord3inddlem  8094  naddcllem  8601  naddasslem1  8619  naddasslem2  8620  elixpsn  8871  frfi  9190  dffi3  9340  ssttrcl  9630  ttrclss  9635  ttrclselem2  9641  fseqenlem1  9937  fpwwe2lem12  10555  hashbc  14378  hashf1lem1  14380  eqs1  14537  cshw1  14746  rpnnen2lem11  16151  drsdirfi  18229  0subg  19048  0subgOLD  19049  0subgALT  19465  efgsp1  19634  dprd2da  19941  lbsextlem4  21086  rnglidl0  21154  ply1coe  22201  mat0dimcrng  22373  txkgen  23555  xkoinjcn  23590  isufil2  23811  ust0  24123  prdsxmetlem  24272  prdsbl  24395  finiunmbl  25461  xrlimcnp  26894  chtub  27139  2sqlem10  27355  dchrisum0flb  27437  pntpbnd1  27513  conway  27728  etasslt  27742  slerec  27748  bday1s  27763  madebdaylemlrcut  27831  precsexlem9  28140  onscutlt  28188  onsiso  28192  n0sfincut  28269  bdayn0p1  28281  zscut  28318  twocut  28333  halfcut  28364  addhalfcut  28365  usgr1e  29208  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  wlkl1loop  29601  crctcshwlkn0lem7  29779  2pthdlem1  29893  rusgrnumwwlkl1  29931  clwwlkccatlem  29951  clwwlkn2  30006  clwwlkel  30008  clwwlkwwlksb  30016  1wlkdlem4  30102  h1deoi  31511  bnj149  34841  subfacp1lem5  35156  cvmlift2lem1  35274  cvmlift2lem12  35286  lindsenlbs  37594  poimirlem28  37627  poimirlem32  37631  heibor1lem  37788  nadd1suc  43365  nregmodel  44991  usgrexmpl1lem  48006  usgrexmpl2lem  48011  isinito2lem  49484  setc1onsubc  49588