Theorem dfqmap2

Description: Alternate definition of the quotient map: QMap in image-of-singleton form. (Contributed by Peter Mazsa, 14-Feb-2026)

	Ref	Expression
Assertion	dfqmap2	⊢ QMap 𝑅 = ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑅 “ { 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		df-qmap	⊢ QMap 𝑅 = ( 𝑥 ∈ dom 𝑅 ↦ [ 𝑥 ] 𝑅 )
2		df-ec	⊢ [ 𝑥 ] 𝑅 = ( 𝑅 “ { 𝑥 } )
3	2	mpteq2i	⊢ ( 𝑥 ∈ dom 𝑅 ↦ [ 𝑥 ] 𝑅 ) = ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑅 “ { 𝑥 } ) )
4	1 3	eqtri	⊢ QMap 𝑅 = ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑅 “ { 𝑥 } ) )