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

Theorem rexsng 4681
Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2139, ax-12 2175. (Revised by GG, 30-Sep-2024.)
Hypothesis
Ref Expression
ralsng.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexsng (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem rexsng
StepHypRef Expression
1 ralsng.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
21notbid 318 . . 3 (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
32ralsng 4680 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓))
4 dfrex2 3071 . . 3 (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑)
5 bicom1 221 . . . 4 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑))
65con1bid 355 . . 3 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑𝜓))
74, 6bitrid 283 . 2 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (∃𝑥 ∈ {𝐴}𝜑𝜓))
83, 7syl 17 1 (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1537  wcel 2106  wral 3059  wrex 3068  {csn 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-sn 4632
This theorem is referenced by:  rexsn  4687  rextpg  4704  iunxsng  5095  frirr  5665  frsn  5776  imasng  6104  naddunif  8730  scshwfzeqfzo  14862  dvdsprmpweqnn  16919  mnd1  18805  grp1  19078  pzriprnglem3  21512  pzriprnglem10  21519  psdmul  22188  cutmax  27983  cutmin  27984  halfcut  28431  elntg2  29015  1loopgrvd0  29537  1egrvtxdg0  29544  nfrgr2v  30301  1vwmgr  30305  elgrplsmsn  33398  grplsmid  33412  ballotlemfc0  34474  ballotlemfcc  34475  bj-restsn  37065  elrnressn  38255  elpaddat  39787  elpadd2at  39789  brfvidRP  43678  mnuunid  44273  iccelpart  47358  zlidlring  48078  lco0  48273
  Copyright terms: Public domain W3C validator