Metamath Proof Explorer

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 = \emptyset \to {({C ↾}_{A}) ↾}_{B} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		reseq2	$⊢ A \cap B = \emptyset \to {C ↾}_{(A \cap B)} = {C ↾}_{\emptyset}$
2		resres	$⊢ {({C ↾}_{A}) ↾}_{B} = {C ↾}_{(A \cap B)}$
3		res0	$⊢ {C ↾}_{\emptyset} = \emptyset$
4	3	eqcomi	$⊢ \emptyset = {C ↾}_{\emptyset}$
5	1 2 4	3eqtr4g	$⊢ A \cap B = \emptyset \to {({C ↾}_{A}) ↾}_{B} = \emptyset$