Theorem eq0 4299

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 2162, ax-12 2182. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2115, df-clel 2808. (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		dfnul4 4284	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
2	1	eqeq2i 2746	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
3		biidd 262	. . . 4 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
4	3	eqabbw 2806	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
5		nbfal 1556	. . . 4 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1820	. . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	4, 6	bitr4i 278	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
8	2, 7	bitri 275	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539   = wceq 1541  ⊥wfal 1553   ∈ wcel 2113  {cab 2711  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-dif 3901  df-nul 4283

This theorem is referenced by:  neq0  4301  nel0  4303  0el  4312  ssdif0  4315  difin0ss  4322  inssdif0  4323  disjiun  5081  0ex  5247  reldm0  5872  iresn0n0  6007  uzwo  12811  hashgt0elex  14310  nrhmzr  20454  zrninitoringc  20593  hausdiag  23561  rnelfmlem  23868  elons2  28196  prv0  35495  wzel  35887  knoppndv  36599  bj-nul  37121  bj-nuliota  37122  bj-nuliotaALT  37123  nninfnub  37812  prtlem14  38994  orddif0suc  43386