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)

	Ref	Expression
Assertion	noel	⊢ ¬ 𝐴 ∈ ∅

Proof

Step	Hyp	Ref	Expression
1		pm3.24	⊢ ¬ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V )
2	1	nex	⊢ ¬ ∃ 𝑦 ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V )
3		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) } ↔ [ 𝑥 / 𝑦 ] ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) )
4		spsbe	⊢ ( [ 𝑥 / 𝑦 ] ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) → ∃ 𝑦 ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) )
5	3 4	sylbi	⊢ ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) } → ∃ 𝑦 ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) )
6	2 5	mto	⊢ ¬ 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) }
7		df-nul	⊢ ∅ = ( V ∖ V )
8		df-dif	⊢ ( V ∖ V ) = { 𝑦 ∣ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) }
9	7 8	eqtri	⊢ ∅ = { 𝑦 ∣ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) }
10	9	eleq2i	⊢ ( 𝑥 ∈ ∅ ↔ 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ V ) } )
11	6 10	mtbir	⊢ ¬ 𝑥 ∈ ∅
12	11	intnan	⊢ ¬ ( 𝑥 = 𝐴 ∧ 𝑥 ∈ ∅ )
13	12	nex	⊢ ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ ∅ )
14		dfclel	⊢ ( 𝐴 ∈ ∅ ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ ∅ ) )
15	13 14	mtbir	⊢ ¬ 𝐴 ∈ ∅