Theorem rexsn 4706

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∃wrex 3076  Vcvv 3488  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-sn 4649

This theorem is referenced by:  elsnres  6050  oarec  8618  snec  8838  zornn0g  10574  fpwwe2lem12  10711  elreal  11200  hashge2el2difr  14530  vdwlem6  17033  pzriprnglem10  21524  pmatcollpw3fi1  22815  restsn  23199  snclseqg  24145  ust0  24249  0slt1s  27892  cuteq1  27896  made0  27930  cofcutr  27976  mulsrid  28157  n0scut  28356  zscut  28411  1p1e2s  28418  nohalf  28425  halfcut  28434  addhalfcut  28437  grplsm0l  33396  rprmdvdsprod  33527  esum2dlem  34056  eulerpartlemgh  34343  eldm3  35723  poimirlem28  37608  heiborlem3  37773  tfsconcatrn  43304