Theorem noel

Description: The empty set has no elements. Theorem 6.14 of Quine p. 44. (Contributed by NM, 21-Jun-1993) (Proof shortened by Mario Carneiro, 1-Sep-2015) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023) (Proof shortened by BJ, 23-Sep-2024) (Proof shortened by BJ, 11-Oct-2026)

	Ref	Expression
Assertion	noel	⊢ ¬ 𝐴 ∈ ∅

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2		dfnul4	⊢ ∅ = { 𝑦 ∣ ⊥ }
3	2	eleq2i	⊢ ( 𝑥 ∈ ∅ ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } )
4		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ [ 𝑥 / 𝑦 ] ⊥ )
5		sbv	⊢ ( [ 𝑥 / 𝑦 ] ⊥ ↔ ⊥ )
6	3 4 5	3bitri	⊢ ( 𝑥 ∈ ∅ ↔ ⊥ )
7	1 6	mtbir	⊢ ¬ 𝑥 ∈ ∅
8	7	nex	⊢ ¬ ∃ 𝑥 𝑥 ∈ ∅
9		elex2	⊢ ( 𝐴 ∈ ∅ → ∃ 𝑥 𝑥 ∈ ∅ )
10	8 9	mto	⊢ ¬ 𝐴 ∈ ∅