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

Theorem rexsn 4687
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 4679 . 2 (𝐴 ∈ V → (∃𝑥 ∈ {𝐴}𝜑𝜓))
41, 3ax-mp 5 1 (∃𝑥 ∈ {𝐴}𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  wrex 3071  Vcvv 3475  {csn 4629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-sn 4630
This theorem is referenced by:  elsnres  6022  oarec  8562  snec  8774  zornn0g  10500  fpwwe2lem12  10637  elreal  11126  hashge2el2difr  14442  vdwlem6  16919  pmatcollpw3fi1  22290  restsn  22674  snclseqg  23620  ust0  23724  0slt1s  27330  cuteq1  27334  made0  27368  cofcutr  27411  mulsrid  27569  grplsm0l  32513  esum2dlem  33090  eulerpartlemgh  33377  eldm3  34731  poimirlem28  36516  heiborlem3  36681  tfsconcatrn  42092  pzriprnglem10  46814
  Copyright terms: Public domain W3C validator