Theorem eq0 4305

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 2840. (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 2838	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4290	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2778	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1578	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1842	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	2, 4, 6	3bitr4i 306	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1561   = wceq 1563  ⊥wfal 1575   ∈ wcel 2145  {cab 2743  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-dif 3910  df-nul 4289

This theorem is referenced by:  neq0  4307  nel0  4310  0el  4319  ssdif0  4322  difin0ss  4329  inssdif0  4330  eq0rdv  4364  rzal  4451  ralf0  4454  disjiun  5092  0ex  5261  reldm0  5908  iresn0n0  6046  uzwo  12923  hashgt0elex  14425  nrhmzr  20610  zrninitoringc  20749  hausdiag  23759  rnelfmlem  24066  elons2  28405  prv0  35788  wzel  36180  knoppndv  36980  bj-nul  37548  bj-nuliota  37549  bj-nuliotaALT  37550  nninfnub  38257  prtlem14  39505  orddif0suc  43852