Theorem bj-0nmoore

Description: The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Assertion	bj-0nmoore	⊢ ¬ ∅ ∈ Moore

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ ∪ ∅ ∈ ∅
2		bj-ismoored0	⊢ ( ∅ ∈ Moore → ∪ ∅ ∈ ∅ )
3	1 2	mto	⊢ ¬ ∅ ∈ Moore