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