This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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