Metamath Proof Explorer

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 R = ( x e. dom R |-> ( R " { x } ) )

Proof

Step Hyp Ref Expression
1 df-qmap 
 |-  QMap R = ( x e. dom R |-> [ x ] R )
2 df-ec 
 |-  [ x ] R = ( R " { x } )
3 2 mpteq2i 
 |-  ( x e. dom R |-> [ x ] R ) = ( x e. dom R |-> ( R " { x } ) )
4 1 3 eqtri 
 |-  QMap R = ( x e. dom R |-> ( R " { x } ) )