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 i^i B ) = (/) -> ( ( C |` A ) |` B ) = (/) )

Proof

Step Hyp Ref Expression
1 reseq2
 |-  ( ( A i^i B ) = (/) -> ( C |` ( A i^i B ) ) = ( C |` (/) ) )
2 resres
 |-  ( ( C |` A ) |` B ) = ( C |` ( A i^i B ) )
3 res0
 |-  ( C |` (/) ) = (/)
4 3 eqcomi
 |-  (/) = ( C |` (/) )
5 1 2 4 3eqtr4g
 |-  ( ( A i^i B ) = (/) -> ( ( C |` A ) |` B ) = (/) )