Theorem eldisjdmqsim2

Description: ElDisj of quotient implies coset-disjointness (domain form). Converts element-disjointness of the quotient carrier into a usable "cosets don't overlap unless equal" rule. (Contributed by Peter Mazsa, 10-Feb-2026)

	Ref	Expression
Assertion	eldisjdmqsim2	|- ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldisjim3	|- ( ElDisj ( dom R /. R ) -> ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )
2		eceldmqs	|- ( R e. Rels -> ( [ u ] R e. ( dom R /. R ) <-> u e. dom R ) )
3		eceldmqs	|- ( R e. Rels -> ( [ v ] R e. ( dom R /. R ) <-> v e. dom R ) )
4	2 3	anbi12d	|- ( R e. Rels -> ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) <-> ( u e. dom R /\ v e. dom R ) ) )
5	4	imbi1d	|- ( R e. Rels -> ( ( ( [ u ] R e. ( dom R /. R ) /\ [ v ] R e. ( dom R /. R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) <-> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) ) )
6	1 5	imbitrid	|- ( R e. Rels -> ( ElDisj ( dom R /. R ) -> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) ) )
7	6	impcom	|- ( ( ElDisj ( dom R /. R ) /\ R e. Rels ) -> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) )