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 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∃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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  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  6011  oarec  8575  snec  8804  zornn0g  10588  fpwwe2lem12  10732  elreal  11221  hashge2el2difr  14631  vdwlem6  17171  pzriprnglem10  21803  pmatcollpw3fi1  23113  restsn  23495  snclseqg  24442  ust0  24546  0lt1s  28205  cuteq1  28210  made0  28256  cofcutr  28317  mulsrid  28506  n0cut  28727  n0fincut  28748  zcuts  28800  twocut  28816  halfcut  28851  addhalfcut  28852  pw2cut2  28855  domnprodeq0  33888  grplsm0l  34002  rprmdvdsprod  34114  esum2dlem  34772  eulerpartlemgh  35058  eldm3  36620  poimirlem28  38673  heiborlem3  38854  tfsconcatrn  44451  nregmodel  46114  stgr1  49166  setc1onsubc  50847