Theorem eq0 4303

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 2191, ax-12 2212. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2144, df-clel 2837. (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 2835	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3		dfnul4 4287	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2775	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		nbfal 1584	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
6	5	albii 1848	. 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 2142  {cab 2740  ∅c0 4285

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-dif 3907  df-nul 4286

This theorem is used by:  neq0  4305  nel0  4308  0el  4317  ssdif0  4320  difin0ss  4327  inssdif0OLD  4329  eq0rdv  4371  rzal  4454  ralf0  4457  disjiun  5096  0ex  5269  reldm0  5917  iresn0n0  6055  uzwo  12941  hashgt0elex  14444  nrhmzr  20647  zrninitoringc  20786  hausdiag  23813  rnelfmlem  24120  elons2  28462  prv0  35930  wzel  36322  knoppndv  37151  bj-nul  37720  bj-nuliota  37721  bj-nuliotaALT  37722  nninfnub  38430  prtlem14  39676  orddif0suc  44023