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 ) = (/) ) |
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 ) = (/) ) |