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	Could not format assertion : No typesetting found for |- ( A e. dom R -> [ A ] QMap R = ( { A } /. R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ecqmap	Could not format ( A e. dom R -> [ A ] QMap R = { [ A ] R } ) : No typesetting found for |- ( A e. dom R -> [ A ] QMap R = { [ A ] R } ) with typecode |-
2		snecg	$$⊢A\in \mathrm{dom}R\to \left\{\left[A\right]R\right\}=\left\{A\right\}/R$$
3	1 2	eqtrd	Could not format ( A e. dom R -> [ A ] QMap R = ( { A } /. R ) ) : No typesetting found for |- ( A e. dom R -> [ A ] QMap R = ( { A } /. R ) ) with typecode |-