Description: Domain of a composition. (Contributed by NM, 19-Mar-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | dmcoeq | |- ( dom A = ran B -> dom ( A o. B ) = dom B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss2 | |- ( dom A = ran B -> ran B C_ dom A ) |
|
2 | dmcosseq | |- ( ran B C_ dom A -> dom ( A o. B ) = dom B ) |
|
3 | 1 2 | syl | |- ( dom A = ran B -> dom ( A o. B ) = dom B ) |