Theorem rexsn 4614

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∃wrex 3063  Vcvv 3431  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-sn 4556

This theorem is referenced by:  elsnres  5973  oarec  8487  snec  8715  zornn0g  10418  fpwwe2lem12  10556  elreal  11045  hashge2el2difr  14434  vdwlem6  16948  pzriprnglem10  21465  pmatcollpw3fi1  22771  restsn  23153  snclseqg  24099  ust0  24203  0lt1s  27822  cuteq1  27827  made0  27873  cofcutr  27934  mulsrid  28123  n0cut  28344  n0fincut  28365  zcuts  28417  twocut  28433  halfcut  28468  addhalfcut  28469  pw2cut2  28472  domnprodeq0  33357  grplsm0l  33486  rprmdvdsprod  33617  esum2dlem  34276  eulerpartlemgh  34562  eldm3  35989  poimirlem28  38015  heiborlem3  38180  tfsconcatrn  43787  nregmodel  45461  stgr1  48452  setc1onsubc  50092