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	Could not format assertion : No typesetting found for |- ran QMap R = ( dom R /. R ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-qmap	Could not format QMap R = ( x e. dom R |-> [ x ] R ) : No typesetting found for |- QMap R = ( x e. dom R |-> [ x ] R ) with typecode |-
2	1	rneqi	Could not format ran QMap R = ran ( x e. dom R |-> [ x ] R ) : No typesetting found for |- ran QMap R = ran ( x e. dom R |-> [ x ] R ) with typecode |-
3		dfqs2	$$⊢\mathrm{dom}R/R=\mathrm{ran}\left(x\in \mathrm{dom}R⟼\left[x\right]R\right)$$
4	2 3	eqtr4i	Could not format ran QMap R = ( dom R /. R ) : No typesetting found for |- ran QMap R = ( dom R /. R ) with typecode |-