Description: Domain of a composition. (Contributed by NM, 19-Mar-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | dmcoeq | ⊢ ( dom 𝐴 = ran 𝐵 → dom ( 𝐴 ∘ 𝐵 ) = dom 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss2 | ⊢ ( dom 𝐴 = ran 𝐵 → ran 𝐵 ⊆ dom 𝐴 ) | |
2 | dmcosseq | ⊢ ( ran 𝐵 ⊆ dom 𝐴 → dom ( 𝐴 ∘ 𝐵 ) = dom 𝐵 ) | |
3 | 1 2 | syl | ⊢ ( dom 𝐴 = ran 𝐵 → dom ( 𝐴 ∘ 𝐵 ) = dom 𝐵 ) |