Theorem ralsn 4648

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-sn 4593

This theorem is referenced by:  xpord2indlem  8129  xpord3inddlem  8136  naddcllem  8643  naddasslem1  8661  naddasslem2  8662  elixpsn  8913  frfi  9239  dffi3  9389  ssttrcl  9675  ttrclss  9680  ttrclselem2  9686  fseqenlem1  9984  fpwwe2lem12  10602  hashbc  14425  hashf1lem1  14427  eqs1  14584  cshw1  14794  rpnnen2lem11  16199  drsdirfi  18273  0subg  19090  0subgOLD  19091  0subgALT  19505  efgsp1  19674  dprd2da  19981  lbsextlem4  21078  rnglidl0  21146  ply1coe  22192  mat0dimcrng  22364  txkgen  23546  xkoinjcn  23581  isufil2  23802  ust0  24114  prdsxmetlem  24263  prdsbl  24386  finiunmbl  25452  xrlimcnp  26885  chtub  27130  2sqlem10  27346  dchrisum0flb  27428  pntpbnd1  27504  conway  27718  etasslt  27732  slerec  27738  bday1s  27750  madebdaylemlrcut  27817  precsexlem9  28124  onscutlt  28172  onsiso  28176  n0sfincut  28253  bdayn0p1  28265  zscut  28302  twocut  28316  halfcut  28340  addhalfcut  28341  usgr1e  29179  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  wlkl1loop  29573  crctcshwlkn0lem7  29753  2pthdlem1  29867  rusgrnumwwlkl1  29905  clwwlkccatlem  29925  clwwlkn2  29980  clwwlkel  29982  clwwlkwwlksb  29990  1wlkdlem4  30076  h1deoi  31485  bnj149  34872  subfacp1lem5  35178  cvmlift2lem1  35296  cvmlift2lem12  35308  lindsenlbs  37616  poimirlem28  37649  poimirlem32  37653  heibor1lem  37810  nadd1suc  43388  nregmodel  45014  usgrexmpl1lem  48016  usgrexmpl2lem  48021  isinito2lem  49491  setc1onsubc  49595