Metamath Proof Explorer


Theorem dmcoeq

Description: Domain of a composition. (Contributed by NM, 19-Mar-1998)

Ref Expression
Assertion dmcoeq ( dom 𝐴 = ran 𝐵 → dom ( 𝐴𝐵 ) = dom 𝐵 )

Proof

Step Hyp Ref Expression
1 eqimss2 ( dom 𝐴 = ran 𝐵 → ran 𝐵 ⊆ dom 𝐴 )
2 dmcosseq ( ran 𝐵 ⊆ dom 𝐴 → dom ( 𝐴𝐵 ) = dom 𝐵 )
3 1 2 syl ( dom 𝐴 = ran 𝐵 → dom ( 𝐴𝐵 ) = dom 𝐵 )