Theorem dmcoeq

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

	Ref	Expression
Assertion	dmcoeq	$$⊢\mathrm{dom}A=\mathrm{ran}B\to \mathrm{dom}\left(A\circ B\right)=\mathrm{dom}B$$

Proof

Step	Hyp	Ref	Expression
1		eqimss2	$$⊢\mathrm{dom}A=\mathrm{ran}B\to \mathrm{ran}B\subseteq \mathrm{dom}A$$
2		dmcosseq	$$⊢\mathrm{ran}B\subseteq \mathrm{dom}A\to \mathrm{dom}\left(A\circ B\right)=\mathrm{dom}B$$
3	1 2	syl	$$⊢\mathrm{dom}A=\mathrm{ran}B\to \mathrm{dom}\left(A\circ B\right)=\mathrm{dom}B$$