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 2197, ax-12 2216. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2149, df-clel 2839. (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 2837	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4283	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2776	. 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 2147  {cab 2741  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-dif 4050  df-nul 4282

This theorem is used by:  neq0  4302  nel0  4305  0el  4314  ssdif0  4317  difin0ss  4324  inssdif0OLD  4326  eq0rdv  4368  rzal  4453  ralf0  4456  disjiun  5094  0ex  5265  reldm0  5918  iresn0n0  6059  uzwo  13068  hashgt0elex  14575  nrhmzr  20822  zrninitoringc  20961  hausdiag  23997  rnelfmlem  24304  elons2  28677  prv0  36375  elpssmo  36649  wzel  36777  knoppndv  37591  bj-nul  38175  bj-nuliota  38176  bj-nuliotaALT  38177  nninfnub  38888  prtlem14  40134  orddif0suc  44473