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

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

Proof of Theorem abn0
StepHypRef Expression
1 ab0 4334 . . 3 ({𝑥𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
21notbii 319 . 2 (¬ {𝑥𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3 df-ne 2944 . 2 ({𝑥𝜑} ≠ ∅ ↔ ¬ {𝑥𝜑} = ∅)
4 df-ex 1782 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
52, 3, 43bitr4i 302 1 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wal 1539   = wceq 1541  wex 1781  {cab 2713  wne 2943  c0 4282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-ne 2944  df-dif 3913  df-nul 4283
This theorem is referenced by:  intexab  5296  iinexg  5298  relimasn  6036  inisegn0  6050  mapprc  8769  modom  9188  tz9.1c  9666  scott0  9822  scott0s  9824  cp  9827  karden  9831  acnrcl  9978  aceq3lem  10056  cff  10184  cff1  10194  cfss  10201  domtriomlem  10378  axdclem  10455  nqpr  10950  supadd  12123  supmul  12127  hashf1lem2  14355  hashf1  14356  mreiincl  17476  efgval  19499  efger  19500  birthdaylem3  26303  disjex  31510  disjexc  31511  mppsval  34166  mblfinlem3  36117  ismblfin  36119  itg2addnc  36132  sdclem1  36202  upbdrech  43529
  Copyright terms: Public domain W3C validator