Theorem rnqmap

Description: The range of the quotient map is the quotient carrier. It lets us replace quotient-carrier reasoning by map/range reasoning (and conversely) via df-qmap and dfqs2 . (Contributed by Peter Mazsa, 12-Feb-2026)

	Ref	Expression
Assertion	rnqmap	⊢ ran QMap 𝑅 = ( dom 𝑅 / 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-qmap	⊢ QMap 𝑅 = ( 𝑥 ∈ dom 𝑅 ↦ [ 𝑥 ] 𝑅 )
2	1	rneqi	⊢ ran QMap 𝑅 = ran ( 𝑥 ∈ dom 𝑅 ↦ [ 𝑥 ] 𝑅 )
3		dfqs2	⊢ ( dom 𝑅 / 𝑅 ) = ran ( 𝑥 ∈ dom 𝑅 ↦ [ 𝑥 ] 𝑅 )
4	2 3	eqtr4i	⊢ ran QMap 𝑅 = ( dom 𝑅 / 𝑅 )