Theorem ecqmap2

Description: Fiber of QMap equals singleton quotient: a conceptual bridge between "map fibers" and quotients. (Contributed by Peter Mazsa, 19-Feb-2026)

	Ref	Expression
Assertion	ecqmap2	|- ( A e. dom R -> [ A ] QMap R = ( { A } /. R ) )

Proof

Step	Hyp	Ref	Expression
1		ecqmap	|- ( A e. dom R -> [ A ] QMap R = { [ A ] R } )
2		snecg	|- ( A e. dom R -> { [ A ] R } = ( { A } /. R ) )
3	1 2	eqtrd	|- ( A e. dom R -> [ A ] QMap R = ( { A } /. R ) )