Theorem ralsn 4526

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522   ∈ wcel 2081  ∀wral 3105  Vcvv 3437  {csn 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-v 3439  df-sbc 3707  df-sn 4473

This theorem is referenced by:  elixpsn  8349  frfi  8609  dffi3  8741  fseqenlem1  9296  fpwwe2lem13  9910  hashbc  13659  hashf1lem1  13661  eqs1  13810  cshw1  14020  rpnnen2lem11  15410  drsdirfi  17377  0subg  18058  efgsp1  18590  dprd2da  18881  lbsextlem4  19623  ply1coe  20147  mat0dimcrng  20763  txkgen  21944  xkoinjcn  21979  isufil2  22200  ust0  22511  prdsxmetlem  22661  prdsbl  22784  finiunmbl  23828  xrlimcnp  25228  chtub  25470  2sqlem10  25686  dchrisum0flb  25768  pntpbnd1  25844  usgr1e  26710  nbgr2vtx1edg  26815  nbuhgr2vtx1edgb  26817  wlkl1loop  27102  crctcshwlkn0lem7  27281  2pthdlem1  27396  rusgrnumwwlkl1  27434  clwwlkccatlem  27454  clwwlkn2  27509  clwwlkel  27512  clwwlkwwlksb  27520  1wlkdlem4  27606  h1deoi  29017  bnj149  31763  subfacp1lem5  32039  cvmlift2lem1  32157  cvmlift2lem12  32169  conway  32873  etasslt  32883  slerec  32886  lindsenlbs  34418  poimirlem28  34451  poimirlem32  34455  heibor1lem  34619