Metamath Proof Explorer

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 \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \leftrightarrow A = B))$

Proof

Step	Hyp	Ref	Expression
1		disjimeceqim2	$⊢ Disj R \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \to A = B))$
2		eceq1	$⊢ A = B \to [A] R = [B] R$
3	2	2a1i	$⊢ Disj R \to ((A \in dom R \land B \in dom R) \to (A = B \to [A] R = [B] R))$
4	1 3	impbidd	$⊢ Disj R \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \leftrightarrow A = B))$