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

Theorem eq0 4305
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.)
Assertion
Ref Expression
eq0 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem eq0
StepHypRef Expression
1 nfcv 2974 . 2 𝑥𝐴
21eq0f 4302 1 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wal 1526   = wceq 1528  wcel 2105  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-dif 3936  df-nul 4289
This theorem is referenced by:  nel0  4308  0el  4317  ssdif0  4320  difin0ss  4325  inssdif0  4326  ralf0  4453  disjiun  5044  0ex  5202  reldm0  5791  iresn0n0  5916  uzwo  12299  hashgt0elex  13750  hausdiag  22181  rnelfmlem  22488  prv0  32574  wzel  33008  knoppndv  33770  bj-ab0  34121  bj-nul  34243  bj-nuliota  34244  bj-nuliotaALT  34245  nninfnub  34907  prtlem14  35890  nrhmzr  44072  zrninitoringc  44270
  Copyright terms: Public domain W3C validator