Theorem rexsn 4630

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∃wrex 3056  Vcvv 3436  {csn 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-v 3438  df-sn 4572

This theorem is referenced by:  elsnres  5965  oarec  8472  snec  8697  zornn0g  10391  fpwwe2lem12  10528  elreal  11017  hashge2el2difr  14383  vdwlem6  16893  pzriprnglem10  21422  pmatcollpw3fi1  22698  restsn  23080  snclseqg  24026  ust0  24130  0slt1s  27768  cuteq1  27773  made0  27813  cofcutr  27863  mulsrid  28047  n0scut  28257  n0sfincut  28277  zscut  28326  1p1e2s  28334  twocut  28341  halfcut  28373  addhalfcut  28374  pw2cut2  28377  grplsm0l  33360  rprmdvdsprod  33491  esum2dlem  34097  eulerpartlemgh  34383  eldm3  35797  poimirlem28  37688  heiborlem3  37853  tfsconcatrn  43375  nregmodel  45050  stgr1  47992  setc1onsubc  49634