Theorem rexsn 4646

Description: Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.)

Hypotheses

Ref	Expression
ralsn.1	⊢ 𝐴 ∈ V
ralsn.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rexsn	⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexsn

Step	Hyp	Ref	Expression
1		ralsn.1	. 2 ⊢ 𝐴 ∈ V
2		ralsn.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	rexsng 4640	. 2 ⊢ (𝐴 ∈ V → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  Vcvv 3447  {csn 4589

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-sn 4590

This theorem is referenced by:  elsnres  5992  oarec  8526  snec  8751  zornn0g  10458  fpwwe2lem12  10595  elreal  11084  hashge2el2difr  14446  vdwlem6  16957  pzriprnglem10  21400  pmatcollpw3fi1  22675  restsn  23057  snclseqg  24003  ust0  24107  0slt1s  27741  cuteq1  27746  made0  27785  cofcutr  27832  mulsrid  28016  n0scut  28226  n0sfincut  28246  zscut  28295  1p1e2s  28302  twocut  28309  halfcut  28333  addhalfcut  28334  grplsm0l  33374  rprmdvdsprod  33505  esum2dlem  34082  eulerpartlemgh  34369  eldm3  35748  poimirlem28  37642  heiborlem3  37807  tfsconcatrn  43331  nregmodel  45007  stgr1  47960  setc1onsubc  49591