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

Theorem rexsng 4364
Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
Hypothesis
Ref Expression
ralsng.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexsng (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem rexsng
StepHypRef Expression
1 rexsns 4362 . 2 (∃𝑥 ∈ {𝐴}𝜑[𝐴 / 𝑥]𝜑)
2 ralsng.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3610 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
41, 3syl5bb 272 1 (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wcel 2140  wrex 3052  [wsbc 3577  {csn 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rex 3057  df-v 3343  df-sbc 3578  df-sn 4323
This theorem is referenced by:  rexsn  4368  rexprg  4380  rextpg  4382  iunxsng  4755  frirr  5244  frsn  5347  imasng  5646  scshwfzeqfzo  13793  dvdsprmpweqnn  15812  mnd1  17553  grp1  17744  1loopgrvd0  26632  1egrvtxdg0  26639  nfrgr2v  27448  1vwmgr  27452  ballotlemfc0  30885  ballotlemfcc  30886  bj-restsn  33360  elpaddat  35612  elpadd2at  35614  brfvidRP  38501  iccelpart  41898  zlidlring  42457  lco0  42745
  Copyright terms: Public domain W3C validator