Theorem ralsn 4622

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2109  ∀wral 3065  Vcvv 3430  {csn 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3432  df-sn 4567

This theorem is referenced by:  elixpsn  8699  frfi  9020  dffi3  9151  ssttrcl  9434  ttrclss  9439  ttrclselem2  9445  fseqenlem1  9764  fpwwe2lem12  10382  hashbc  14146  hashf1lem1  14149  hashf1lem1OLD  14150  eqs1  14298  cshw1  14516  rpnnen2lem11  15914  drsdirfi  18004  0subg  18761  efgsp1  19324  dprd2da  19626  lbsextlem4  20404  ply1coe  21448  mat0dimcrng  21600  txkgen  22784  xkoinjcn  22819  isufil2  23040  ust0  23352  prdsxmetlem  23502  prdsbl  23628  finiunmbl  24689  xrlimcnp  26099  chtub  26341  2sqlem10  26557  dchrisum0flb  26639  pntpbnd1  26715  usgr1e  27593  nbgr2vtx1edg  27698  nbuhgr2vtx1edgb  27700  wlkl1loop  27985  crctcshwlkn0lem7  28160  2pthdlem1  28274  rusgrnumwwlkl1  28312  clwwlkccatlem  28332  clwwlkn2  28387  clwwlkel  28389  clwwlkwwlksb  28397  1wlkdlem4  28483  h1deoi  29890  bnj149  32834  subfacp1lem5  33125  cvmlift2lem1  33243  cvmlift2lem12  33255  xpord2ind  33773  xpord3ind  33779  naddcllem  33810  conway  33972  etasslt  33986  slerec  33992  bday1s  34004  madebdaylemlrcut  34058  lindsenlbs  35751  poimirlem28  35784  poimirlem32  35788  heibor1lem  35946