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

Theorem rexsng 4675
Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2140, ax-12 2176. (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 4674 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓))
4 dfrex2 3072 . . 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 1539  wcel 2107  wral 3060  wrex 3069  {csn 4625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-v 3481  df-sn 4626
This theorem is referenced by:  rexsn  4681  rextpg  4698  iunxsng  5089  frirr  5660  frsn  5772  imasng  6101  naddunif  8732  scshwfzeqfzo  14866  dvdsprmpweqnn  16924  mnd1  18793  grp1  19066  pzriprnglem3  21495  pzriprnglem10  21502  psdmul  22171  cutmax  27969  cutmin  27970  halfcut  28417  elntg2  29001  1loopgrvd0  29523  1egrvtxdg0  29530  nfrgr2v  30292  1vwmgr  30296  elgrplsmsn  33419  grplsmid  33433  ballotlemfc0  34496  ballotlemfcc  34497  bj-restsn  37084  elrnressn  38275  elpaddat  39807  elpadd2at  39809  brfvidRP  43706  mnuunid  44301  iccelpart  47425  zlidlring  48155  lco0  48349
  Copyright terms: Public domain W3C validator