Theorem eq0 4299

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 2160, ax-12 2180. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2113, df-clel 2806. (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 4284	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
2	1	eqeq2i 2744	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
3		biidd 262	. . . 4 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
4	3	eqabbw 2804	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
5		nbfal 1556	. . . 4 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1820	. . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	4, 6	bitr4i 278	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
8	2, 7	bitri 275	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539   = wceq 1541  ⊥wfal 1553   ∈ wcel 2111  {cab 2709  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-dif 3900  df-nul 4283

This theorem is referenced by:  neq0  4301  nel0  4303  0el  4312  ssdif0  4315  difin0ss  4322  inssdif0  4323  disjiun  5081  0ex  5247  reldm0  5873  iresn0n0  6008  uzwo  12815  hashgt0elex  14314  nrhmzr  20458  zrninitoringc  20597  hausdiag  23566  rnelfmlem  23873  elons2  28201  prv0  35481  wzel  35873  knoppndv  36585  bj-nul  37107  bj-nuliota  37108  bj-nuliotaALT  37109  nninfnub  37797  prtlem14  38979  orddif0suc  43366