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

Theorem eq0 4141
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 2959 . 2 𝑥𝐴
21eq0f 4138 1 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wal 1635   = wceq 1637  wcel 2157  c0 4127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-dif 3783  df-nul 4128
This theorem is referenced by:  nel0  4144  0el  4151  ssdif0  4154  difin0ss  4158  inssdif0  4159  ralf0  4283  disjiun  4843  0ex  4997  reldm0  5558  uzwo  11990  hashgt0elex  13426  hausdiag  21683  rnelfmlem  21990  wzel  32112  unblimceq0  32837  knoppndv  32864  bj-ab0  33229  bj-nul  33347  bj-nuliota  33348  bj-nuliotaALT  33349  nninfnub  33877  prtlem14  34672  nrhmzr  42459  zrninitoringc  42657
  Copyright terms: Public domain W3C validator