Theorem resdisj

Description: A double restriction to disjoint classes is the empty set. (Contributed by NM, 7-Oct-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	resdisj	$$⊢A\cap B=\varnothing \to {\left({C\upharpoonright }_A\right)\upharpoonright }_B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		reseq2	$$⊢A\cap B=\varnothing \to {C\upharpoonright }_{\left(A\cap B\right)}={C\upharpoonright }_{\varnothing }$$
2		resres	$$⊢{\left({C\upharpoonright }_A\right)\upharpoonright }_B={C\upharpoonright }_{\left(A\cap B\right)}$$
3		res0	$$⊢{C\upharpoonright }_{\varnothing }=\varnothing$$
4	3	eqcomi	$$⊢\varnothing ={C\upharpoonright }_{\varnothing }$$
5	1 2 4	3eqtr4g	$$⊢A\cap B=\varnothing \to {\left({C\upharpoonright }_A\right)\upharpoonright }_B=\varnothing$$