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