Theorem eq0 4296

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 2193, ax-12 2212. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2146, df-clel 2835. (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 265	. . 3 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
2	1	eqabbw 2833	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4280	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2773	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1584	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1851	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
7	2, 4, 6	3bitr4i 306	1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1567   = wceq 1569  ⊥wfal 1581   ∈ wcel 2144  {cab 2738  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-dif 4047  df-nul 4279

This theorem is used by:  neq0  4298  nel0  4301  0el  4310  ssdif0  4313  difin0ss  4320  inssdif0OLD  4322  eq0rdv  4364  rzal  4449  ralf0  4452  disjiun  5090  0ex  5260  reldm0  5909  iresn0n0  6045  uzwo  13042  hashgt0elex  14549  nrhmzr  20795  zrninitoringc  20934  hausdiag  23970  rnelfmlem  24277  elons2  28650  prv0  36282  wzel  36679  knoppndv  37493  bj-nul  38064  bj-nuliota  38065  bj-nuliotaALT  38066  nninfnub  38779  prtlem14  40025  orddif0suc  44364