Theorem rexsn 4636

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3057  Vcvv 3437  {csn 4577

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-v 3439  df-sn 4578

This theorem is referenced by:  elsnres  5977  oarec  8486  snec  8711  zornn0g  10407  fpwwe2lem12  10544  elreal  11033  hashge2el2difr  14395  vdwlem6  16905  pzriprnglem10  21436  pmatcollpw3fi1  22723  restsn  23105  snclseqg  24051  ust0  24155  0slt1s  27793  cuteq1  27798  made0  27838  cofcutr  27888  mulsrid  28072  n0scut  28282  n0sfincut  28302  zscut  28351  1p1e2s  28359  twocut  28366  halfcut  28398  addhalfcut  28399  pw2cut2  28402  domnprodeq0  33286  grplsm0l  33412  rprmdvdsprod  33543  esum2dlem  34177  eulerpartlemgh  34463  eldm3  35877  poimirlem28  37761  heiborlem3  37926  tfsconcatrn  43499  nregmodel  45174  stgr1  48123  setc1onsubc  49763