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

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

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