Theorem ralsn 4645

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3078  Vcvv 3453  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-sn 4588

This theorem is used by:  xpord2indlem  8149  xpord3inddlem  8156  naddcllem  8668  naddasslem1  8687  naddasslem2  8688  elixpsn  8948  frfi  9259  dffi3  9405  ssttrcl  9698  ttrclss  9703  ttrclselem2  9709  fseqenlem1  10031  fpwwe2lem12  10655  hashbc  14522  hashf1lem1  14524  eqs1  14684  cshw1  14897  rpnnen2lem11  16318  drsdirfi  18399  0subg  19281  0subgALT  19701  efgsp1  19870  dprd2da  20177  lbsextlem4  21354  rnglidl0  21424  lindsenlbs  22070  ply1coe  22529  mat0dimcrng  22698  txkgen  23884  xkoinjcn  23919  isufil2  24140  ust0  24452  prdsxmetlem  24600  prdsbl  24723  finiunmbl  25778  xrlimcnp  27213  chtub  27456  2sqlem10  27672  dchrisum0flb  27754  pntpbnd1  27830  conway  28052  etaslts  28066  lesrec  28072  bday1  28087  madebdaylemlrcut  28172  precsexlem9  28488  oncutlt  28537  oniso  28544  n0fincut  28628  bdayn0p1  28642  zcuts  28680  twocut  28696  halfcut  28731  addhalfcut  28732  pw2cut2  28735  1reno  28770  usgr1e  29713  nbgr2vtx1edg  29818  nbuhgr2vtx1edgb  29820  wlkl1loop  30105  crctcshwlkn0lem7  30292  2pthdlem1  30406  rusgrnumwwlkl1  30447  clwwlkccatlem  30467  clwwlkn2  30522  clwwlkel  30524  clwwlkwwlksb  30532  1wlkdlem4  30618  h1deoi  32038  selvply1rhmlemb  34037  vieta  34098  bnj149  35392  subfacp1lem5  35771  cvmlift2lem1  35889  cvmlift2lem12  35901  nmulrid  36785  poimirlem28  38405  poimirlem32  38409  heibor1lem  38567  nadd1suc  44241  nregmodel  45848  usgrexmpl1lem  48945  usgrexmpl2lem  48950  isinito2lem  50432  setc1onsubc  50536