Theorem ralsn 4652

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∀wral 3082  Vcvv 3458  {csn 4594

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-v 3460  df-sn 4595

This theorem is used by:  xpord2indlem  8152  xpord3inddlem  8159  naddcllem  8671  naddasslem1  8690  naddasslem2  8691  elixpsn  8944  frfi  9255  dffi3  9401  ssttrcl  9694  ttrclss  9699  ttrclselem2  9705  fseqenlem1  10027  fpwwe2lem12  10645  hashbc  14510  hashf1lem1  14512  eqs1  14672  cshw1  14885  rpnnen2lem11  16305  drsdirfi  18386  0subg  19249  0subgALT  19669  efgsp1  19838  dprd2da  20145  lbsextlem4  21322  rnglidl0  21392  ply1coe  22495  mat0dimcrng  22664  txkgen  23846  xkoinjcn  23881  isufil2  24102  ust0  24414  prdsxmetlem  24562  prdsbl  24685  finiunmbl  25740  xrlimcnp  27170  chtub  27413  2sqlem10  27629  dchrisum0flb  27711  pntpbnd1  27787  conway  28009  etaslts  28023  lesrec  28029  bday1  28044  madebdaylemlrcut  28129  precsexlem9  28445  oncutlt  28494  oniso  28501  n0fincut  28585  bdayn0p1  28599  zcuts  28637  twocut  28653  halfcut  28688  addhalfcut  28689  pw2cut2  28692  1reno  28727  usgr1e  29632  nbgr2vtx1edg  29737  nbuhgr2vtx1edgb  29739  wlkl1loop  30024  crctcshwlkn0lem7  30202  2pthdlem1  30316  rusgrnumwwlkl1  30357  clwwlkccatlem  30377  clwwlkn2  30432  clwwlkel  30434  clwwlkwwlksb  30442  1wlkdlem4  30528  h1deoi  31938  selvply1rhmlemb  33940  vieta  34001  bnj149  35295  subfacp1lem5  35697  cvmlift2lem1  35815  cvmlift2lem12  35827  nmulrid  36710  lindsenlbs  38307  poimirlem28  38340  poimirlem32  38344  heibor1lem  38501  nadd1suc  44160  nregmodel  45767  usgrexmpl1lem  48827  usgrexmpl2lem  48832  isinito2lem  50317  setc1onsubc  50421