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

Theorem rexsng 4640
Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 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 4639 . 2 (𝐴𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓))
4 dfrex2 3077 . . 3 (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑)
5 bicom1 220 . . . 4 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑))
65con1bid 356 . . 3 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑𝜓))
74, 6bitrid 283 . 2 ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (∃𝑥 ∈ {𝐴}𝜑𝜓))
83, 7syl 17 1 (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1542  wcel 2107  wral 3065  wrex 3074  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-v 3450  df-sn 4592
This theorem is referenced by:  rexsn  4648  rextpg  4665  iunxsng  5055  frirr  5615  frsn  5724  imasng  6040  naddunif  8644  scshwfzeqfzo  14722  dvdsprmpweqnn  16764  mnd1  18604  grp1  18861  elntg2  27976  1loopgrvd0  28494  1egrvtxdg0  28501  nfrgr2v  29258  1vwmgr  29262  elgrplsmsn  32211  grplsmid  32225  ballotlemfc0  33132  ballotlemfcc  33133  bj-restsn  35582  elrnressn  36762  elpaddat  38296  elpadd2at  38298  brfvidRP  42034  mnuunid  42631  iccelpart  45699  zlidlring  46300  lco0  46582
  Copyright terms: Public domain W3C validator