Theorem eq0 4274

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 2156, ax-12 2173. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2110, df-clel 2817. (Revised by Gino Giotto, 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		dfnul4 4255	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
2	1	eqeq2i 2751	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
3		dfcleq 2731	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
4		df-clab 2716	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
5		sbv 2092	. . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
6	4, 5	bitri 274	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
7	6	bibi2i 337	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
8		nbfal 1554	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
9	7, 8	bitr4i 277	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ¬ 𝑥 ∈ 𝐴)
10	9	albii 1823	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
11	3, 10	bitri 274	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
12	2, 11	bitri 274	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537   = wceq 1539  ⊥wfal 1551  [wsb 2068   ∈ wcel 2108  {cab 2715  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-dif 3886  df-nul 4254

This theorem is referenced by:  neq0  4276  nel0  4281  0el  4291  ssdif0  4294  difin0ss  4299  inssdif0  4300  ralf0OLD  4445  disjiun  5057  0ex  5226  reldm0  5826  iresn0n0  5952  uzwo  12580  hashgt0elex  14044  hausdiag  22704  rnelfmlem  23011  prv0  33292  wzel  33745  knoppndv  34641  bj-nul  35154  bj-nuliota  35155  bj-nuliotaALT  35156  nninfnub  35836  prtlem14  36815  nrhmzr  45319  zrninitoringc  45517