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

Theorem eq0 3962
 Description: The empty set 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 2793 . 2 𝑥𝐴
21eq0f 3958 1 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1521   = wceq 1523   ∈ wcel 2030  ∅c0 3948 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-nul 3949 This theorem is referenced by:  nel0  3965  0el  3972  ssdif0  3975  difin0ss  3979  inssdif0  3980  ralf0  4111  ralf0OLD  4112  disjiun  4672  0ex  4823  reldm0  5375  uzwo  11789  hashgt0elex  13227  hausdiag  21496  rnelfmlem  21803  wzel  31894  unblimceq0  32623  knoppndv  32650  bj-ab0  33027  bj-nul  33143  bj-nuliota  33144  bj-nuliotaALT  33145  nninfnub  33677  prtlem14  34478  nrhmzr  42198  zrninitoringc  42396
 Copyright terms: Public domain W3C validator