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

Theorem abn0 4385
Description: Nonempty class abstraction. See also ab0 4380. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2816, ax-8 2110. (Revised by GG, 30-Aug-2024.)
Assertion
Ref Expression
abn0 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Proof of Theorem abn0
StepHypRef Expression
1 ab0 4380 . . 3 ({𝑥𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
21notbii 320 . 2 (¬ {𝑥𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3 df-ne 2941 . 2 ({𝑥𝜑} ≠ ∅ ↔ ¬ {𝑥𝜑} = ∅)
4 df-ex 1780 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
52, 3, 43bitr4i 303 1 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1538   = wceq 1540  wex 1779  {cab 2714  wne 2940  c0 4333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-ne 2941  df-dif 3954  df-nul 4334
This theorem is referenced by:  intexab  5346  iinexg  5348  relimasn  6103  inisegn0  6116  mapprc  8870  modom  9280  tz9.1c  9770  scott0  9926  scott0s  9928  cp  9931  karden  9935  acnrcl  10082  aceq3lem  10160  cff  10288  cff1  10298  cfss  10305  domtriomlem  10482  axdclem  10559  nqpr  11054  supadd  12236  supmul  12240  hashf1lem2  14495  hashf1  14496  mreiincl  17639  efgval  19735  efger  19736  birthdaylem3  26996  disjex  32605  disjexc  32606  mppsval  35577  mblfinlem3  37666  ismblfin  37668  itg2addnc  37681  sdclem1  37750  upbdrech  45317
  Copyright terms: Public domain W3C validator