Theorem eq0 4291

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 2163, ax-12 2185. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2116, df-clel 2812. (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 262	. . 3 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
2	1	eqabbw 2810	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4276	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2750	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1557	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1821	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	2, 4, 6	3bitr4i 303	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540   = wceq 1542  ⊥wfal 1554   ∈ wcel 2114  {cab 2715  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-dif 3893  df-nul 4275

This theorem is referenced by:  neq0  4293  nel0  4295  0el  4304  ssdif0  4307  difin0ss  4314  inssdif0  4315  eq0rdv  4348  rzal  4435  ralf0  4438  disjiun  5074  0ex  5242  reldm0  5877  iresn0n0  6013  uzwo  12852  hashgt0elex  14354  nrhmzr  20505  zrninitoringc  20644  hausdiag  23620  rnelfmlem  23927  elons2  28264  prv0  35628  wzel  36020  knoppndv  36810  bj-nul  37379  bj-nuliota  37380  bj-nuliotaALT  37381  nninfnub  38086  prtlem14  39334  orddif0suc  43714