Theorem rexsn 4686

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∃wrex 3067  Vcvv 3477  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-v 3479  df-sn 4631

This theorem is referenced by:  elsnres  6040  oarec  8598  snec  8818  zornn0g  10542  fpwwe2lem12  10679  elreal  11168  hashge2el2difr  14516  vdwlem6  17019  pzriprnglem10  21518  pmatcollpw3fi1  22809  restsn  23193  snclseqg  24139  ust0  24243  0slt1s  27888  cuteq1  27892  made0  27926  cofcutr  27972  mulsrid  28153  n0scut  28352  zscut  28407  1p1e2s  28414  nohalf  28421  halfcut  28430  addhalfcut  28433  grplsm0l  33410  rprmdvdsprod  33541  esum2dlem  34072  eulerpartlemgh  34359  eldm3  35740  poimirlem28  37634  heiborlem3  37799  tfsconcatrn  43331  stgr1  47863