Theorem rexsn 4627

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3430  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-sn 4569

This theorem is referenced by:  elsnres  5980  oarec  8490  snec  8718  zornn0g  10418  fpwwe2lem12  10556  elreal  11045  hashge2el2difr  14434  vdwlem6  16948  pzriprnglem10  21480  pmatcollpw3fi1  22763  restsn  23145  snclseqg  24091  ust0  24195  0lt1s  27818  cuteq1  27823  made0  27869  cofcutr  27930  mulsrid  28119  n0cut  28340  n0fincut  28361  zcuts  28413  twocut  28429  halfcut  28464  addhalfcut  28465  pw2cut2  28468  domnprodeq0  33352  grplsm0l  33478  rprmdvdsprod  33609  esum2dlem  34252  eulerpartlemgh  34538  eldm3  35959  poimirlem28  37983  heiborlem3  38148  tfsconcatrn  43788  nregmodel  45462  stgr1  48449  setc1onsubc  50089