Theorem eq0 4285

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 2168, ax-12 2189. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2121, df-clel 2815. (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 263	. . 3 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
2	1	eqabbw 2813	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4270	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2753	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1562	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1826	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	2, 4, 6	3bitr4i 304	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545   = wceq 1547  ⊥wfal 1559   ∈ wcel 2119  {cab 2718  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-dif 3893  df-nul 4269

This theorem is referenced by:  neq0  4287  nel0  4289  0el  4298  ssdif0  4301  difin0ss  4308  inssdif0  4309  eq0rdv  4342  rzal  4429  ralf0  4432  disjiun  5067  0ex  5236  reldm0  5877  iresn0n0  6013  uzwo  12859  hashgt0elex  14361  nrhmzr  20516  zrninitoringc  20655  hausdiag  23635  rnelfmlem  23942  elons2  28275  prv0  35665  wzel  36057  knoppndv  36847  bj-nul  37416  bj-nuliota  37417  bj-nuliotaALT  37418  nninfnub  38125  prtlem14  39373  orddif0suc  43720