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

Theorem rexsn 4170
Description: Restricted existential quantification over a singleton. (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 4166 . 2 (𝐴 ∈ V → (∃𝑥 ∈ {𝐴}𝜑𝜓))
41, 3ax-mp 5 1 (∃𝑥 ∈ {𝐴}𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  wcel 1977  wrex 2897  Vcvv 3173  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-sbc 3403  df-sn 4126
This theorem is referenced by:  elsnres  5356  oarec  7529  snec  7697  zornn0g  9210  fpwwe2lem13  9343  elreal  9831  hashge2el2difr  13118  vdwlem6  15528  pmatcollpw3fi1  20412  restsn  20784  snclseqg  21729  ust0  21833  esum2dlem  29481  eulerpartlemgh  29767  eldm3  30905  poimirlem28  32607  heiborlem3  32782
  Copyright terms: Public domain W3C validator