Theorem eq0 4305

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.) Avoid ax-11 2192, ax-12 2213. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2145, df-clel 2838. (Revised by GG, 6-Sep-2024.)

Assertion

Ref	Expression
eq0	⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem eq0

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		biidd 265	. . 3 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
2	1	eqabbw 2836	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4289	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2776	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1585	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1849	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	2, 4, 6	3bitr4i 306	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ⊥wfal 1582   ∈ wcel 2143  {cab 2741  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-dif 3909  df-nul 4288

This theorem is referenced by:  neq0  4307  nel0  4310  0el  4319  ssdif0  4322  difin0ss  4329  inssdif0OLD  4331  eq0rdv  4373  rzal  4456  ralf0  4459  disjiun  5098  0ex  5271  reldm0  5920  iresn0n0  6058  uzwo  12936  hashgt0elex  14439  nrhmzr  20623  zrninitoringc  20762  hausdiag  23783  rnelfmlem  24090  elons2  28432  prv0  35903  wzel  36295  knoppndv  37104  bj-nul  37673  bj-nuliota  37674  bj-nuliotaALT  37675  nninfnub  38383  prtlem14  39629  orddif0suc  43978