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

Theorem rexsn 4580
 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 4574 . 2 (𝐴 ∈ V → (∃𝑥 ∈ {𝐴}𝜑𝜓))
41, 3ax-mp 5 1 (∃𝑥 ∈ {𝐴}𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∃wrex 3107  Vcvv 3441  {csn 4525 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rex 3112  df-v 3443  df-sbc 3721  df-sn 4526 This theorem is referenced by:  elsnres  5859  oarec  8178  snec  8350  zornn0g  9923  fpwwe2lem12  10060  elreal  10549  hashge2el2difr  13842  vdwlem6  16319  pmatcollpw3fi1  21407  restsn  21789  snclseqg  22735  ust0  22839  grplsm0l  31030  esum2dlem  31497  eulerpartlemgh  31782  eldm3  33146  poimirlem28  35125  heiborlem3  35291
 Copyright terms: Public domain W3C validator