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	Could not format assertion : No typesetting found for |- QMap R = ( x e. dom R |-> ( R " { x } ) ) 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		df-ec	$$⊢\left[x\right]R=R\left[\left\{x\right\}\right]$$
3	2	mpteq2i	$$⊢\left(x\in \mathrm{dom}R⟼\left[x\right]R\right)=\left(x\in \mathrm{dom}R⟼R\left[\left\{x\right\}\right]\right)$$
4	1 3	eqtri	Could not format QMap R = ( x e. dom R |-> ( R " { x } ) ) : No typesetting found for |- QMap R = ( x e. dom R |-> ( R " { x } ) ) with typecode |-