Theorem eq0 4141

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 2959	. 2 ⊢ Ⅎ𝑥𝐴
2	1	eq0f 4138	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 197  ∀wal 1635   = wceq 1637   ∈ wcel 2157  ∅c0 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-dif 3783  df-nul 4128

This theorem is referenced by:  nel0  4144  0el  4151  ssdif0  4154  difin0ss  4158  inssdif0  4159  ralf0  4283  disjiun  4843  0ex  4997  reldm0  5558  uzwo  11990  hashgt0elex  13426  hausdiag  21683  rnelfmlem  21990  wzel  32112  unblimceq0  32837  knoppndv  32864  bj-ab0  33229  bj-nul  33347  bj-nuliota  33348  bj-nuliotaALT  33349  nninfnub  33877  prtlem14  34672  nrhmzr  42459  zrninitoringc  42657