Theorem rexsn 4663

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3061  Vcvv 3464  {csn 4606

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-v 3466  df-sn 4607

This theorem is referenced by:  elsnres  6013  oarec  8579  snec  8799  zornn0g  10524  fpwwe2lem12  10661  elreal  11150  hashge2el2difr  14504  vdwlem6  17011  pzriprnglem10  21456  pmatcollpw3fi1  22731  restsn  23113  snclseqg  24059  ust0  24163  0slt1s  27798  cuteq1  27803  made0  27842  cofcutr  27889  mulsrid  28073  n0scut  28283  n0sfincut  28303  zscut  28352  1p1e2s  28359  twocut  28366  halfcut  28390  addhalfcut  28391  grplsm0l  33423  rprmdvdsprod  33554  esum2dlem  34128  eulerpartlemgh  34415  eldm3  35783  poimirlem28  37677  heiborlem3  37842  tfsconcatrn  43333  stgr1  47940  setc1onsubc  49446