Theorem rexsn 4643

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-sn 4585

This theorem is used by:  elsnres  6014  oarec  8549  snec  8778  zornn0g  10507  fpwwe2lem12  10651  elreal  11140  hashge2el2difr  14546  vdwlem6  17078  pzriprnglem10  21703  pmatcollpw3fi1  23013  restsn  23395  snclseqg  24342  ust0  24446  0lt1s  28077  cuteq1  28082  made0  28128  cofcutr  28189  mulsrid  28378  n0cut  28599  n0fincut  28620  zcuts  28672  twocut  28688  halfcut  28723  addhalfcut  28724  pw2cut2  28727  domnprodeq0  33719  grplsm0l  33832  rprmdvdsprod  33944  esum2dlem  34602  eulerpartlemgh  34889  eldm3  36340  poimirlem28  38397  heiborlem3  38563  tfsconcatrn  44183  nregmodel  45840  stgr1  48877  setc1onsubc  50528