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

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

Proof of Theorem rexsng
StepHypRef Expression
1 nfv 1908 . 2 𝑥𝜓
2 ralsng.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rexsngf 4602 1 (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   = wceq 1530   ∈ wcel 2107  ∃wrex 3137  {csn 4559 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-v 3495  df-sbc 3771  df-sn 4560 This theorem is referenced by:  rexsn  4612  rextpg  4627  iunxsng  5003  frirr  5525  frsn  5632  imasng  5944  scshwfzeqfzo  14180  dvdsprmpweqnn  16213  mnd1  17944  grp1  18198  elntg2  26763  1loopgrvd0  27278  1egrvtxdg0  27285  nfrgr2v  28043  1vwmgr  28047  elgrplsmsn  30937  ballotlemfc0  31738  ballotlemfcc  31739  bj-restsn  34360  elpaddat  36922  elpadd2at  36924  brfvidRP  40013  mnuunid  40593  iccelpart  43573  zlidlring  44179  lco0  44462
 Copyright terms: Public domain W3C validator