Theorem int0el

Description: The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	int0el	⊢ ( ∅ ∈ 𝐴 → ∩ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		intss1	⊢ ( ∅ ∈ 𝐴 → ∩ 𝐴 ⊆ ∅ )
2		0ss	⊢ ∅ ⊆ ∩ 𝐴
3	2	a1i	⊢ ( ∅ ∈ 𝐴 → ∅ ⊆ ∩ 𝐴 )
4	1 3	eqssd	⊢ ( ∅ ∈ 𝐴 → ∩ 𝐴 = ∅ )