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 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ↔ 𝐴 = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjimeceqim2	⊢ ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
2		eceq1	⊢ ( 𝐴 = 𝐵 → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
3	2	2a1i	⊢ ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( 𝐴 = 𝐵 → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) ) )
4	1 3	impbidd	⊢ ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ↔ 𝐴 = 𝐵 ) ) )