Theorem rexsn 4636

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

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

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 3440  df-sn 4580

This theorem is referenced by:  elsnres  5976  oarec  8487  snec  8712  zornn0g  10418  fpwwe2lem12  10555  elreal  11044  hashge2el2difr  14407  vdwlem6  16917  pzriprnglem10  21416  pmatcollpw3fi1  22692  restsn  23074  snclseqg  24020  ust0  24124  0slt1s  27762  cuteq1  27767  made0  27806  cofcutr  27856  mulsrid  28040  n0scut  28250  n0sfincut  28270  zscut  28319  1p1e2s  28327  twocut  28334  halfcut  28365  addhalfcut  28366  grplsm0l  33359  rprmdvdsprod  33490  esum2dlem  34078  eulerpartlemgh  34365  eldm3  35753  poimirlem28  37647  heiborlem3  37812  tfsconcatrn  43335  nregmodel  45011  stgr1  47965  setc1onsubc  49607