Theorem rexsn 4639

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3060  Vcvv 3440  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-v 3442  df-sn 4581

This theorem is referenced by:  elsnres  5980  oarec  8489  snec  8715  zornn0g  10415  fpwwe2lem12  10553  elreal  11042  hashge2el2difr  14404  vdwlem6  16914  pzriprnglem10  21445  pmatcollpw3fi1  22732  restsn  23114  snclseqg  24060  ust0  24164  0lt1s  27808  cuteq1  27813  made0  27859  cofcutr  27920  mulsrid  28109  n0cut  28330  n0fincut  28351  zcuts  28403  twocut  28419  halfcut  28454  addhalfcut  28455  pw2cut2  28458  domnprodeq0  33358  grplsm0l  33484  rprmdvdsprod  33615  esum2dlem  34249  eulerpartlemgh  34535  eldm3  35955  poimirlem28  37849  heiborlem3  38014  tfsconcatrn  43584  nregmodel  45258  stgr1  48207  setc1onsubc  49847