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	$$⊢\varnothing \cap A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		incom	$$⊢\varnothing \cap A=A\cap \varnothing$$
2		in0	$$⊢A\cap \varnothing =\varnothing$$
3	1 2	eqtri	$$⊢\varnothing \cap A=\varnothing$$