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 R = ( dom R /. R )

Proof

Step	Hyp	Ref	Expression
1		df-qmap	|- QMap R = ( x e. dom R |-> [ x ] R )
2	1	rneqi	|- ran QMap R = ran ( x e. dom R |-> [ x ] R )
3		dfqs2	|- ( dom R /. R ) = ran ( x e. dom R |-> [ x ] R )
4	2 3	eqtr4i	|- ran QMap R = ( dom R /. R )