Theorem ralsn 4642

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-sn 4585

This theorem is used by:  xpord2indlem  8148  xpord3inddlem  8155  naddcllem  8669  naddasslem1  8688  naddasslem2  8689  elixpsn  8949  frfi  9260  dffi3  9407  ssttrcl  9700  ttrclss  9705  ttrclselem2  9711  fseqenlem1  10084  fpwwe2lem12  10708  hashbc  14578  hashf1lem1  14580  eqs1  14740  cshw1  14953  rpnnen2lem11  16372  drsdirfi  18459  0subg  19342  0subgALT  19762  efgsp1  19931  dprd2da  20238  lbsextlem4  21419  rnglidl0  21489  lindsenlbs  22137  ply1coe  22596  mat0dimcrng  22765  txkgen  23951  xkoinjcn  23986  isufil2  24207  ust0  24519  prdsxmetlem  24667  prdsbl  24790  finiunmbl  25845  xrlimcnp  27278  chtub  27521  2sqlem10  27737  dchrisum0flb  27819  pntpbnd1  27895  conway  28147  etaslts  28161  lesrec  28167  bday1  28182  madebdaylemlrcut  28267  precsexlem9  28583  oncutlt  28632  oniso  28639  n0fincut  28723  bdayn0p1  28737  zcuts  28775  twocut  28791  halfcut  28826  addhalfcut  28827  pw2cut2  28830  1reno  28865  usgr1e  29808  nbgr2vtx1edg  29913  nbuhgr2vtx1edgb  29915  wlkl1loop  30200  crctcshwlkn0lem7  30387  2pthdlem1  30501  rusgrnumwwlkl1  30542  clwwlkccatlem  30562  clwwlkn2  30617  clwwlkel  30619  clwwlkwwlksb  30627  1wlkdlem4  30713  h1deoi  32133  selvply1rhmlemb  34133  vieta  34194  bnj149  35488  subfacp1lem5  35918  cvmlift2lem1  36036  cvmlift2lem12  36048  nmulrid  36916  poimirlem28  38534  poimirlem32  38538  heibor1lem  38711  nadd1suc  44352  nregmodel  45959  usgrexmpl1lem  49063  usgrexmpl2lem  49068  isinito2lem  50550  setc1onsubc  50654