Theorem 0in

Description: The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	0in	⊢ ( ∅ ∩ 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		incom	⊢ ( ∅ ∩ 𝐴 ) = ( 𝐴 ∩ ∅ )
2		in0	⊢ ( 𝐴 ∩ ∅ ) = ∅
3	1 2	eqtri	⊢ ( ∅ ∩ 𝐴 ) = ∅