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 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∃wrex 3095  Vcvv 3463  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-sn 4592

This theorem is referenced by:  elsnres  6018  oarec  8543  snec  8772  zornn0g  10485  fpwwe2lem12  10623  elreal  11112  hashge2el2difr  14514  vdwlem6  17042  pzriprnglem10  21605  pmatcollpw3fi1  22910  restsn  23292  snclseqg  24238  ust0  24342  0lt1s  27967  cuteq1  27972  made0  28018  cofcutr  28079  mulsrid  28268  n0cut  28489  n0fincut  28510  zcuts  28562  twocut  28578  halfcut  28613  addhalfcut  28614  pw2cut2  28617  domnprodeq0  33536  grplsm0l  33652  rprmdvdsprod  33765  esum2dlem  34423  eulerpartlemgh  34709  eldm3  36148  poimirlem28  38182  heiborlem3  38347  tfsconcatrn  43956  nregmodel  45613  stgr1  48610  setc1onsubc  50260