Theorem ralsn 4647

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 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3060  Vcvv 3446  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3448  df-sn 4592

This theorem is referenced by:  xpord2indlem  8084  xpord3inddlem  8091  naddcllem  8627  naddasslem1  8645  naddasslem2  8646  elixpsn  8882  frfi  9239  dffi3  9376  ssttrcl  9660  ttrclss  9665  ttrclselem2  9671  fseqenlem1  9969  fpwwe2lem12  10587  hashbc  14362  hashf1lem1  14365  hashf1lem1OLD  14366  eqs1  14512  cshw1  14722  rpnnen2lem11  16117  drsdirfi  18208  0subg  18967  0subgOLD  18968  0subgALT  19364  efgsp1  19533  dprd2da  19835  lbsextlem4  20681  ply1coe  21704  mat0dimcrng  21856  txkgen  23040  xkoinjcn  23075  isufil2  23296  ust0  23608  prdsxmetlem  23758  prdsbl  23884  finiunmbl  24945  xrlimcnp  26355  chtub  26597  2sqlem10  26813  dchrisum0flb  26895  pntpbnd1  26971  conway  27181  etasslt  27195  slerec  27201  bday1s  27213  madebdaylemlrcut  27271  usgr1e  28256  nbgr2vtx1edg  28361  nbuhgr2vtx1edgb  28363  wlkl1loop  28649  crctcshwlkn0lem7  28824  2pthdlem1  28938  rusgrnumwwlkl1  28976  clwwlkccatlem  28996  clwwlkn2  29051  clwwlkel  29053  clwwlkwwlksb  29061  1wlkdlem4  29147  h1deoi  30554  bnj149  33576  subfacp1lem5  33865  cvmlift2lem1  33983  cvmlift2lem12  33995  lindsenlbs  36146  poimirlem28  36179  poimirlem32  36183  heibor1lem  36341  nadd1suc  41785