Theorem eq0 4325

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 2157, ax-12 2177. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2110, df-clel 2809. (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		dfnul4 4310	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
2	1	eqeq2i 2748	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
3		dfcleq 2728	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
4		df-clab 2714	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
5		sbv 2088	. . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
6	4, 5	bitri 275	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
7	6	bibi2i 337	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
8		nbfal 1555	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
9	7, 8	bitr4i 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ¬ 𝑥 ∈ 𝐴)
10	9	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
11	3, 10	bitri 275	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
12	2, 11	bitri 275	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538   = wceq 1540  ⊥wfal 1552  [wsb 2064   ∈ wcel 2108  {cab 2713  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-dif 3929  df-nul 4309

This theorem is referenced by:  neq0  4327  nel0  4329  0el  4338  ssdif0  4341  difin0ss  4348  inssdif0  4349  disjiun  5107  0ex  5277  reldm0  5907  iresn0n0  6041  uzwo  12925  hashgt0elex  14417  nrhmzr  20495  zrninitoringc  20634  hausdiag  23581  rnelfmlem  23888  elons2  28198  prv0  35398  wzel  35788  knoppndv  36498  bj-nul  37020  bj-nuliota  37021  bj-nuliotaALT  37022  nninfnub  37721  prtlem14  38838  orddif0suc  43239