Description: Absorption law for restriction. (Contributed by NM, 27-Mar-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | resabs2 | |- ( B C_ C -> ( ( A |` B ) |` C ) = ( A |` B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rescom | |- ( ( A |` B ) |` C ) = ( ( A |` C ) |` B ) |
|
2 | resabs1 | |- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) ) |
|
3 | 1 2 | eqtrid | |- ( B C_ C -> ( ( A |` B ) |` C ) = ( A |` B ) ) |