MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexsn Structured version   Visualization version   GIF version

Theorem rexsn 4682
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
StepHypRef Expression
1 ralsn.1 . 2 𝐴 ∈ V
2 ralsn.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32rexsng 4676 . 2 (𝐴 ∈ V → (∃𝑥 ∈ {𝐴}𝜑𝜓))
41, 3ax-mp 5 1 (∃𝑥 ∈ {𝐴}𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wcel 2108  wrex 3070  Vcvv 3480  {csn 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-sn 4627
This theorem is referenced by:  elsnres  6039  oarec  8600  snec  8820  zornn0g  10545  fpwwe2lem12  10682  elreal  11171  hashge2el2difr  14520  vdwlem6  17024  pzriprnglem10  21501  pmatcollpw3fi1  22794  restsn  23178  snclseqg  24124  ust0  24228  0slt1s  27874  cuteq1  27878  made0  27912  cofcutr  27958  mulsrid  28139  n0scut  28338  zscut  28393  1p1e2s  28400  nohalf  28407  halfcut  28416  addhalfcut  28419  grplsm0l  33431  rprmdvdsprod  33562  esum2dlem  34093  eulerpartlemgh  34380  eldm3  35761  poimirlem28  37655  heiborlem3  37820  tfsconcatrn  43355  stgr1  47928
  Copyright terms: Public domain W3C validator