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

Proof

Step	Hyp	Ref	Expression
1		qmapeldisjsim	Could not format ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) : No typesetting found for |- ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) ) with typecode |-
2		eceq1	$$⊢A=B\to \left[A\right]R=\left[B\right]R$$
3	1 2	impbid1	Could not format ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R <-> A = B ) ) : No typesetting found for |- ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R <-> A = B ) ) with typecode |-