Theorem dmcoss2

Description: The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018)

	Ref	Expression
Assertion	dmcoss2	⊢ dom ≀ 𝑅 = ran 𝑅

Proof

Step	Hyp	Ref	Expression
1		dmcoss3	⊢ dom ≀ 𝑅 = dom ◡ 𝑅
2		df-rn	⊢ ran 𝑅 = dom ◡ 𝑅
3	1 2	eqtr4i	⊢ dom ≀ 𝑅 = ran 𝑅