Theorem eq0 4297

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 2194, ax-12 2213. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2147, df-clel 2836. (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 2834	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4281	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2774	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1585	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1852	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	2, 4, 6	3bitr4i 306	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ⊥wfal 1582   ∈ wcel 2145  {cab 2739  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-dif 3902  df-nul 4280

This theorem is used by:  neq0  4299  nel0  4302  0el  4311  ssdif0  4314  difin0ss  4321  inssdif0OLD  4323  eq0rdv  4365  rzal  4450  ralf0  4453  disjiun  5091  0ex  5261  reldm0  5910  iresn0n0  6048  uzwo  13019  hashgt0elex  14525  nrhmzr  20769  zrninitoringc  20908  hausdiag  23944  rnelfmlem  24251  elons2  28626  prv0  36164  wzel  36556  knoppndv  37370  bj-nul  37939  bj-nuliota  37940  bj-nuliotaALT  37941  nninfnub  38653  prtlem14  39899  orddif0suc  44228