Theorem rexsn 4682

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∃wrex 3070  Vcvv 3480  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-sn 4627

This theorem is referenced by:  elsnres  6039  oarec  8600  snec  8820  zornn0g  10545  fpwwe2lem12  10682  elreal  11171  hashge2el2difr  14520  vdwlem6  17024  pzriprnglem10  21501  pmatcollpw3fi1  22794  restsn  23178  snclseqg  24124  ust0  24228  0slt1s  27874  cuteq1  27878  made0  27912  cofcutr  27958  mulsrid  28139  n0scut  28338  zscut  28393  1p1e2s  28400  nohalf  28407  halfcut  28416  addhalfcut  28419  grplsm0l  33431  rprmdvdsprod  33562  esum2dlem  34093  eulerpartlemgh  34380  eldm3  35761  poimirlem28  37655  heiborlem3  37820  tfsconcatrn  43355  stgr1  47928