Theorem rncoeq

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

	Ref	Expression
Assertion	rncoeq	⊢ ( dom 𝐴 = ran 𝐵 → ran ( 𝐴 ∘ 𝐵 ) = ran 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dmcoeq	⊢ ( dom ◡ 𝐵 = ran ◡ 𝐴 → dom ( ◡ 𝐵 ∘ ◡ 𝐴 ) = dom ◡ 𝐴 )
2		eqcom	⊢ ( dom 𝐴 = ran 𝐵 ↔ ran 𝐵 = dom 𝐴 )
3		df-rn	⊢ ran 𝐵 = dom ◡ 𝐵
4		dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴
5	3 4	eqeq12i	⊢ ( ran 𝐵 = dom 𝐴 ↔ dom ◡ 𝐵 = ran ◡ 𝐴 )
6	2 5	bitri	⊢ ( dom 𝐴 = ran 𝐵 ↔ dom ◡ 𝐵 = ran ◡ 𝐴 )
7		df-rn	⊢ ran ( 𝐴 ∘ 𝐵 ) = dom ◡ ( 𝐴 ∘ 𝐵 )
8		cnvco	⊢ ◡ ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ 𝐴 )
9	8	dmeqi	⊢ dom ◡ ( 𝐴 ∘ 𝐵 ) = dom ( ◡ 𝐵 ∘ ◡ 𝐴 )
10	7 9	eqtri	⊢ ran ( 𝐴 ∘ 𝐵 ) = dom ( ◡ 𝐵 ∘ ◡ 𝐴 )
11		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
12	10 11	eqeq12i	⊢ ( ran ( 𝐴 ∘ 𝐵 ) = ran 𝐴 ↔ dom ( ◡ 𝐵 ∘ ◡ 𝐴 ) = dom ◡ 𝐴 )
13	1 6 12	3imtr4i	⊢ ( dom 𝐴 = ran 𝐵 → ran ( 𝐴 ∘ 𝐵 ) = ran 𝐴 )