Theorem rexsn 4638

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∃wrex 3085  Vcvv 3453  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-v 3455  df-sn 4580

This theorem is referenced by:  elsnres  6003  oarec  8525  snec  8754  zornn0g  10456  fpwwe2lem12  10594  elreal  11083  hashge2el2difr  14488  vdwlem6  17013  pzriprnglem10  21530  pmatcollpw3fi1  22836  restsn  23218  snclseqg  24164  ust0  24268  0lt1s  27893  cuteq1  27898  made0  27944  cofcutr  28005  mulsrid  28194  n0cut  28415  n0fincut  28436  zcuts  28488  twocut  28504  halfcut  28539  addhalfcut  28540  pw2cut2  28543  domnprodeq0  33421  grplsm0l  33550  rprmdvdsprod  33691  esum2dlem  34350  eulerpartlemgh  34636  eldm3  36072  poimirlem28  38108  heiborlem3  38273  tfsconcatrn  43880  nregmodel  45554  stgr1  48544  setc1onsubc  50184