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	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐶 ↾ 𝐴 ) ↾ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		reseq2	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐶 ↾ ∅ ) )
2		resres	⊢ ( ( 𝐶 ↾ 𝐴 ) ↾ 𝐵 ) = ( 𝐶 ↾ ( 𝐴 ∩ 𝐵 ) )
3		res0	⊢ ( 𝐶 ↾ ∅ ) = ∅
4	3	eqcomi	⊢ ∅ = ( 𝐶 ↾ ∅ )
5	1 2 4	3eqtr4g	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐶 ↾ 𝐴 ) ↾ 𝐵 ) = ∅ )