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

Theorem eq0 4194
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 2932 . 2 𝑥𝐴
21eq0f 4191 1 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wal 1505   = wceq 1507  wcel 2050  c0 4178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-11 2093  ax-12 2106  ax-ext 2750
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-dif 3832  df-nul 4179
This theorem is referenced by:  nel0  4197  0el  4206  ssdif0  4209  difin0ss  4214  inssdif0  4215  ralf0  4340  disjiun  4917  0ex  5068  reldm0  5641  uzwo  12125  hashgt0elex  13575  hausdiag  21957  rnelfmlem  22264  wzel  32638  knoppndv  33399  bj-ab0  33722  bj-nul  33866  bj-nuliota  33867  bj-nuliotaALT  33868  nninfnub  34474  prtlem14  35461  nrhmzr  43514  zrninitoringc  43712
  Copyright terms: Public domain W3C validator