Theorem ralsn 4366

Description: Convert a quantification over 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 4362	. 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2139  ∀wral 3050  Vcvv 3340  {csn 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-v 3342  df-sbc 3577  df-sn 4322

This theorem is referenced by:  elixpsn  8113  frfi  8370  dffi3  8502  fseqenlem1  9037  fpwwe2lem13  9656  hashbc  13429  hashf1lem1  13431  eqs1  13583  cshw1  13768  rpnnen2lem11  15152  drsdirfi  17139  0subg  17820  efgsp1  18350  dprd2da  18641  lbsextlem4  19363  ply1coe  19868  mat0dimcrng  20478  txkgen  21657  xkoinjcn  21692  isufil2  21913  ust0  22224  prdsxmetlem  22374  prdsbl  22497  finiunmbl  23512  xrlimcnp  24894  chtub  25136  2sqlem10  25352  dchrisum0flb  25398  pntpbnd1  25474  usgr1e  26336  nbgr2vtx1edg  26445  nbuhgr2vtx1edgb  26447  wlkl1loop  26744  crctcshwlkn0lem7  26919  2pthdlem1  27050  rusgrnumwwlkl1  27090  clwwlkccatlem  27112  clwwlkn2  27173  clwwlkel  27175  clwwlkwwlksb  27184  1wlkdlem4  27292  h1deoi  28717  bnj149  31252  subfacp1lem5  31473  cvmlift2lem1  31591  cvmlift2lem12  31603  conway  32216  etasslt  32226  slerec  32229  lindsenlbs  33717  poimirlem28  33750  poimirlem32  33754  heibor1lem  33921