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 2190, ax-12 2211. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2143, df-clel 2836. (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 264	. . 3 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
2	1	eqabbw 2834	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4285	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2774	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1574	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1838	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	2, 4, 6	3bitr4i 305	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1557   = wceq 1559  ⊥wfal 1571   ∈ wcel 2141  {cab 2739  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-dif 3905  df-nul 4284

This theorem is referenced by:  neq0  4302  nel0  4304  0el  4313  ssdif0  4316  difin0ss  4323  inssdif0  4324  eq0rdv  4358  rzal  4445  ralf0  4448  disjiun  5085  0ex  5254  reldm0  5900  iresn0n0  6038  uzwo  12905  hashgt0elex  14407  nrhmzr  20573  zrninitoringc  20712  hausdiag  23692  rnelfmlem  23999  elons2  28338  prv0  35740  wzel  36132  knoppndv  36932  bj-nul  37501  bj-nuliota  37502  bj-nuliotaALT  37503  nninfnub  38210  prtlem14  39458  orddif0suc  43805