Theorem dfqmap3

Description: Alternate definition of the quotient map: QMap as ordered-pair class abstraction. Gives the raw set-builder characterization for extensional proofs, Rel proofs ( relqmap ), and composition/intersection manipulations. (Contributed by Peter Mazsa, 14-Feb-2026)

	Ref	Expression
Assertion	dfqmap3	|- QMap R = { <. x , y >. | ( x e. dom R /\ y = [ x ] R ) }

Proof

Step	Hyp	Ref	Expression
1		df-qmap	|- QMap R = ( x e. dom R |-> [ x ] R )
2		df-mpt	|- ( x e. dom R |-> [ x ] R ) = { <. x , y >. | ( x e. dom R /\ y = [ x ] R ) }
3	1 2	eqtri	|- QMap R = { <. x , y >. | ( x e. dom R /\ y = [ x ] R ) }