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	⊢ ( 𝐴 ∈ dom 𝑅 → [ 𝐴 ] QMap 𝑅 = ( { 𝐴 } / 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ecqmap	⊢ ( 𝐴 ∈ dom 𝑅 → [ 𝐴 ] QMap 𝑅 = { [ 𝐴 ] 𝑅 } )
2		snecg	⊢ ( 𝐴 ∈ dom 𝑅 → { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 ) )
3	1 2	eqtrd	⊢ ( 𝐴 ∈ dom 𝑅 → [ 𝐴 ] QMap 𝑅 = ( { 𝐴 } / 𝑅 ) )