Theorem rexsn 4640

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  Vcvv 3441  {csn 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-v 3443  df-sn 4582

This theorem is referenced by:  elsnres  5981  oarec  8491  snec  8719  zornn0g  10419  fpwwe2lem12  10557  elreal  11046  hashge2el2difr  14408  vdwlem6  16918  pzriprnglem10  21449  pmatcollpw3fi1  22736  restsn  23118  snclseqg  24064  ust0  24168  0slt1s  27810  cuteq1  27815  made0  27855  cofcutr  27906  mulsrid  28095  n0scut  28314  n0sfincut  28335  zscut  28386  1p1e2s  28395  twocut  28402  halfcut  28437  addhalfcut  28438  pw2cut2  28441  domnprodeq0  33339  grplsm0l  33465  rprmdvdsprod  33596  esum2dlem  34230  eulerpartlemgh  34516  eldm3  35936  poimirlem28  37820  heiborlem3  37985  tfsconcatrn  43620  nregmodel  45294  stgr1  48243  setc1onsubc  49883