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

Theorem eq0 3887
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 2750 . 2 𝑥𝐴
21eq0f 3883 1 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wal 1472   = wceq 1474  wcel 1976  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-nul 3874
This theorem is referenced by:  0el  3894  ssdif0  3895  difin0ss  3899  inssdif0  3900  ralf0  4029  ralf0OLD  4030  disjiun  4567  0ex  4713  dm0  5247  reldm0  5251  uzwo  11583  fzouzdisj  12328  hashgt0elex  13002  hausdiag  21200  rnelfmlem  21508  wzel  30821  wzelOLD  30822  unblimceq0  31474  knoppndv  31501  bj-ab0  31897  bj-nel0  31931  bj-nul  32012  bj-nuliota  32013  bj-nuliotaALT  32014  nninfnub  32520  prtlem14  32980  stoweidlem44  38741  nrhmzr  41665  zrninitoringc  41865
  Copyright terms: Public domain W3C validator