Theorem disjimeceqbi2

Description: Injectivity of the block constructor under disjointness. suc11reg analogue: under disjointness, equal blocks force equal generators (on dom R ). (Contributed by Peter Mazsa, 16-Feb-2026)

	Ref	Expression
Assertion	disjimeceqbi2	|- ( Disj R -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R <-> A = B ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjimeceqim2	|- ( Disj R -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) )
2		eceq1	|- ( A = B -> [ A ] R = [ B ] R )
3	2	2a1i	|- ( Disj R -> ( ( A e. dom R /\ B e. dom R ) -> ( A = B -> [ A ] R = [ B ] R ) ) )
4	1 3	impbidd	|- ( Disj R -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R <-> A = B ) ) )