Theorem rexsn 4650

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∃wrex 3091  Vcvv 3457  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-sn 4592

This theorem is used by:  elsnres  6022  oarec  8549  snec  8778  zornn0g  10500  fpwwe2lem12  10638  elreal  11127  hashge2el2difr  14532  vdwlem6  17064  pzriprnglem10  21670  pmatcollpw3fi1  22975  restsn  23357  snclseqg  24304  ust0  24408  0lt1s  28036  cuteq1  28041  made0  28087  cofcutr  28148  mulsrid  28337  n0cut  28558  n0fincut  28579  zcuts  28631  twocut  28647  halfcut  28682  addhalfcut  28683  pw2cut2  28686  domnprodeq0  33639  grplsm0l  33752  rprmdvdsprod  33864  esum2dlem  34522  eulerpartlemgh  34809  eldm3  36266  poimirlem28  38332  heiborlem3  38497  tfsconcatrn  44102  nregmodel  45759  stgr1  48759  setc1onsubc  50413