Theorem eq0 4307

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 2195, ax-12 2216. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2148, df-clel 2841. (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 2839	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4291	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2779	. 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 2146  {cab 2744  ∅c0 4289

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 2156  ax-ext 2738

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 2745  df-cleq 2758  df-dif 3911  df-nul 4290

This theorem is used by:  neq0  4309  nel0  4312  0el  4321  ssdif0  4324  difin0ss  4331  inssdif0OLD  4333  eq0rdv  4375  rzal  4460  ralf0  4463  disjiun  5102  0ex  5275  reldm0  5923  iresn0n0  6061  uzwo  12953  hashgt0elex  14457  nrhmzr  20673  zrninitoringc  20812  hausdiag  23839  rnelfmlem  24146  elons2  28488  prv0  35943  wzel  36335  knoppndv  37164  bj-nul  37733  bj-nuliota  37734  bj-nuliotaALT  37735  nninfnub  38443  prtlem14  39689  orddif0suc  44036