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

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

Proof of Theorem abn0
StepHypRef Expression
1 ab0 4373 . . 3 ({𝑥𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
21notbii 319 . 2 (¬ {𝑥𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3 df-ne 2931 . 2 ({𝑥𝜑} ≠ ∅ ↔ ¬ {𝑥𝜑} = ∅)
4 df-ex 1775 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
52, 3, 43bitr4i 302 1 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wal 1532   = wceq 1534  wex 1774  {cab 2703  wne 2930  c0 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-ne 2931  df-dif 3950  df-nul 4324
This theorem is referenced by:  intexab  5337  iinexg  5339  relimasn  6085  inisegn0  6099  mapprc  8849  modom  9269  tz9.1c  9764  scott0  9920  scott0s  9922  cp  9925  karden  9929  acnrcl  10076  aceq3lem  10154  cff  10280  cff1  10290  cfss  10297  domtriomlem  10474  axdclem  10551  nqpr  11046  supadd  12226  supmul  12230  hashf1lem2  14468  hashf1  14469  mreiincl  17602  efgval  19709  efger  19710  birthdaylem3  26976  disjex  32510  disjexc  32511  mppsval  35411  mblfinlem3  37371  ismblfin  37373  itg2addnc  37386  sdclem1  37455  upbdrech  44954
  Copyright terms: Public domain W3C validator