Theorem ralsn 4648

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∀wral 3079  Vcvv 3455  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-sn 4591

This theorem is referenced by:  xpord2indlem  8144  xpord3inddlem  8151  naddcllem  8663  naddasslem1  8682  naddasslem2  8683  elixpsn  8936  frfi  9246  dffi3  9392  ssttrcl  9685  ttrclss  9690  ttrclselem2  9696  fseqenlem1  10009  fpwwe2lem12  10628  hashbc  14492  hashf1lem1  14494  eqs1  14652  cshw1  14861  rpnnen2lem11  16281  drsdirfi  18362  0subg  19219  0subgALT  19639  efgsp1  19808  dprd2da  20115  lbsextlem4  21266  rnglidl0  21336  ply1coe  22439  mat0dimcrng  22608  txkgen  23790  xkoinjcn  23825  isufil2  24046  ust0  24358  prdsxmetlem  24506  prdsbl  24629  finiunmbl  25684  xrlimcnp  27111  chtub  27354  2sqlem10  27570  dchrisum0flb  27652  pntpbnd1  27728  conway  27950  etaslts  27964  lesrec  27970  bday1  27985  madebdaylemlrcut  28070  precsexlem9  28386  oncutlt  28435  oniso  28442  n0fincut  28526  bdayn0p1  28540  zcuts  28578  twocut  28594  halfcut  28629  addhalfcut  28630  pw2cut2  28633  1reno  28668  usgr1e  29573  nbgr2vtx1edg  29678  nbuhgr2vtx1edgb  29680  wlkl1loop  29965  crctcshwlkn0lem7  30143  2pthdlem1  30257  rusgrnumwwlkl1  30298  clwwlkccatlem  30318  clwwlkn2  30373  clwwlkel  30375  clwwlkwwlksb  30383  1wlkdlem4  30469  h1deoi  31879  selvply1rhmlemb  33887  vieta  33948  bnj149  35241  subfacp1lem5  35654  cvmlift2lem1  35772  cvmlift2lem12  35784  nmulrid  36675  lindsenlbs  38244  poimirlem28  38277  poimirlem32  38281  heibor1lem  38438  nadd1suc  44099  nregmodel  45706  usgrexmpl1lem  48763  usgrexmpl2lem  48768  isinito2lem  50253  setc1onsubc  50357