Theorem eq0 3888

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

Step	Hyp	Ref	Expression
1		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐴
2	1	eq0f 3884	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wal 1473   = wceq 1475   ∈ wcel 1977  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  0el  3895  ssdif0  3896  difin0ss  3900  inssdif0  3901  ralf0  4030  ralf0OLD  4031  disjiun  4573  0ex  4718  dm0  5260  reldm0  5264  cnv0  5454  uzwo  11627  fzouzdisj  12373  hashgt0elex  13050  hausdiag  21258  rnelfmlem  21566  wzel  31015  wzelOLD  31016  unblimceq0  31668  knoppndv  31695  bj-ab0  32094  bj-nel0  32128  bj-nul  32209  bj-nuliota  32210  bj-nuliotaALT  32211  nninfnub  32717  prtlem14  33177  stoweidlem44  38937  nrhmzr  41663  zrninitoringc  41863