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 3087  Vcvv 3451  {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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-sn 4585

This theorem is used by:  elsnres  6010  oarec  8563  snec  8792  zornn0g  10576  fpwwe2lem12  10720  elreal  11209  hashge2el2difr  14619  vdwlem6  17157  pzriprnglem10  21789  pmatcollpw3fi1  23099  restsn  23481  snclseqg  24428  ust0  24532  0lt1s  28191  cuteq1  28196  made0  28242  cofcutr  28303  mulsrid  28492  n0cut  28713  n0fincut  28734  zcuts  28786  twocut  28802  halfcut  28837  addhalfcut  28838  pw2cut2  28841  domnprodeq0  33833  grplsm0l  33947  rprmdvdsprod  34059  esum2dlem  34717  eulerpartlemgh  35003  eldm3  36505  poimirlem28  38546  heiborlem3  38727  tfsconcatrn  44328  nregmodel  45985  stgr1  49028  setc1onsubc  50679