Theorem eq0 4300

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 2215. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2147, df-clel 2837. (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 2835	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4284	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2775	. 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 2740  ∅c0 4282

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 2734

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 2741  df-cleq 2754  df-dif 3905  df-nul 4283

This theorem is used by:  neq0  4302  nel0  4305  0el  4314  ssdif0  4317  difin0ss  4324  inssdif0OLD  4326  eq0rdv  4368  rzal  4453  ralf0  4456  disjiun  5095  0ex  5268  reldm0  5916  iresn0n0  6054  uzwo  12964  hashgt0elex  14469  nrhmzr  20705  zrninitoringc  20844  hausdiag  23877  rnelfmlem  24184  elons2  28531  prv0  36017  wzel  36409  knoppndv  37239  bj-nul  37808  bj-nuliota  37809  bj-nuliotaALT  37810  nninfnub  38509  prtlem14  39755  orddif0suc  44117