Theorem dmqmap

Description: QMap preserves the domain. Confirms that QMap is defined exactly on the points where cosets [ x ] R make sense (those in dom R ). (Contributed by Peter Mazsa, 14-Feb-2026)

	Ref	Expression
Assertion	dmqmap	|- ( R e. V -> dom QMap R = dom R )

Proof

Step	Hyp	Ref	Expression
1		df-qmap	|- QMap R = ( x e. dom R |-> [ x ] R )
2		ecexg	|- ( R e. V -> [ x ] R e. _V )
3	2	adantr	|- ( ( R e. V /\ x e. dom R ) -> [ x ] R e. _V )
4	1 3	dmmptd	|- ( R e. V -> dom QMap R = dom R )