Theorem ralsn 4681

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  ∀wral 3056  Vcvv 3469  {csn 4624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-v 3471  df-sn 4625

This theorem is referenced by:  xpord2indlem  8146  xpord3inddlem  8153  naddcllem  8690  naddasslem1  8708  naddasslem2  8709  elixpsn  8949  frfi  9306  dffi3  9448  ssttrcl  9732  ttrclss  9737  ttrclselem2  9743  fseqenlem1  10041  fpwwe2lem12  10659  hashbc  14438  hashf1lem1  14441  hashf1lem1OLD  14442  eqs1  14588  cshw1  14798  rpnnen2lem11  16194  drsdirfi  18290  0subg  19099  0subgOLD  19100  0subgALT  19516  efgsp1  19685  dprd2da  19992  lbsextlem4  21042  rnglidl0  21118  ply1coe  22210  mat0dimcrng  22365  txkgen  23549  xkoinjcn  23584  isufil2  23805  ust0  24117  prdsxmetlem  24267  prdsbl  24393  finiunmbl  25466  xrlimcnp  26893  chtub  27138  2sqlem10  27354  dchrisum0flb  27436  pntpbnd1  27512  conway  27725  etasslt  27739  slerec  27745  bday1s  27757  madebdaylemlrcut  27818  precsexlem9  28106  usgr1e  29051  nbgr2vtx1edg  29156  nbuhgr2vtx1edgb  29158  wlkl1loop  29445  crctcshwlkn0lem7  29620  2pthdlem1  29734  rusgrnumwwlkl1  29772  clwwlkccatlem  29792  clwwlkn2  29847  clwwlkel  29849  clwwlkwwlksb  29857  1wlkdlem4  29943  h1deoi  31352  bnj149  34496  subfacp1lem5  34784  cvmlift2lem1  34902  cvmlift2lem12  34914  lindsenlbs  37077  poimirlem28  37110  poimirlem32  37114  heibor1lem  37271  nadd1suc  42793