Metamath Proof Explorer

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	\|- ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		qmapeldisjsim	\|- ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) )
2		eceq1	\|- ( A = B -> [ A ] R = [ B ] R )
3	1 2	impbid1	\|- ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R <-> A = B ) )

Step

Hyp

Ref

Expression

qmapeldisjsim

 |-  ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R -> A = B ) )

eceq1

 |-  ( A = B -> [ A ] R = [ B ] R )

1 2

impbid1

 |-  ( ( R e. V /\ QMap R e. Disjs /\ ( A e. dom R /\ B e. dom R ) ) -> ( [ A ] R = [ B ] R <-> A = B ) )