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

Theorem rexsng 4410
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 4408 . 2 (∃𝑥 ∈ {𝐴}𝜑[𝐴 / 𝑥]𝜑)
2 ralsng.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3666 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
41, 3syl5bb 275 1 (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1653  wcel 2157  wrex 3090  [wsbc 3633  {csn 4368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rex 3095  df-v 3387  df-sbc 3634  df-sn 4369
This theorem is referenced by:  rexsn  4414  rexprg  4425  rextpg  4427  iunxsng  4792  frirr  5289  frsn  5394  imasng  5704  scshwfzeqfzo  13911  dvdsprmpweqnn  15922  mnd1  17646  grp1  17838  1loopgrvd0  26754  1egrvtxdg0  26761  nfrgr2v  27621  1vwmgr  27625  ballotlemfc0  31071  ballotlemfcc  31072  bj-restsn  33528  elpaddat  35825  elpadd2at  35827  brfvidRP  38763  iccelpart  42209  zlidlring  42727  lco0  43015
  Copyright terms: Public domain W3C validator