Theorem qmapeldisjsbi

Description: Injectivity of coset map from QMap being disjoint (biconditional form). Convenience version of qmapeldisjsim . (Contributed by Peter Mazsa, 16-Feb-2026)

	Ref	Expression
Assertion	qmapeldisjsbi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		qmapeldisjsim	⊢ ( ( 𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) )
2		eceq1	⊢ ( 𝐴 = 𝐵 → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
3	1 2	impbid1	⊢ ( ( 𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ↔ 𝐴 = 𝐵 ) )