This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )