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

Theorem eq0 4258
Description: A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2158, ax-12 2175. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.)
Assertion
Ref Expression
eq0 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem eq0
StepHypRef Expression
1 dfcleq 2792 . 2 (𝐴 = ∅ ↔ ∀𝑥(𝑥𝐴𝑥 ∈ ∅))
2 noel 4247 . . . 4 ¬ 𝑥 ∈ ∅
32nbn 376 . . 3 𝑥𝐴 ↔ (𝑥𝐴𝑥 ∈ ∅))
43albii 1821 . 2 (∀𝑥 ¬ 𝑥𝐴 ↔ ∀𝑥(𝑥𝐴𝑥 ∈ ∅))
51, 4bitr4i 281 1 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wal 1536   = wceq 1538  wcel 2111  c0 4243
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-dif 3884  df-nul 4244
This theorem is referenced by:  neq0  4259  nel0  4264  0el  4274  ssdif0  4277  difin0ss  4282  inssdif0  4283  ralf0  4415  disjiun  5017  0ex  5175  reldm0  5762  iresn0n0  5890  uzwo  12299  hashgt0elex  13758  hausdiag  22250  rnelfmlem  22557  prv0  32790  wzel  33224  knoppndv  33986  bj-ab0  34348  bj-nul  34473  bj-nuliota  34474  bj-nuliotaALT  34475  nninfnub  35189  prtlem14  36170  nrhmzr  44495  zrninitoringc  44693
  Copyright terms: Public domain W3C validator