Metamath Proof Explorer

Theorem disjimeceqim2

Description: Disj implies injectivity (pairwise form). The same content as disjimeceqim but packaged for direct use with explicit hypotheses ( A e. dom R /\ B e. dom R ) . (Contributed by Peter Mazsa, 16-Feb-2026)

		Ref	Expression
	Assertion	disjimeceqim2	$⊢ Disj R \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \to A = B))$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ (Disj R \land (A \in dom R \land B \in dom R)) \to A \in dom R$
2		simprr	$⊢ (Disj R \land (A \in dom R \land B \in dom R)) \to B \in dom R$
3		eleq1	$⊢ u = A \to (u \in dom R \leftrightarrow A \in dom R)$
4		eleq1	$⊢ v = B \to (v \in dom R \leftrightarrow B \in dom R)$
5	3 4	bi2anan9	$⊢ (u = A \land v = B) \to ((u \in dom R \land v \in dom R) \leftrightarrow (A \in dom R \land B \in dom R))$
6		eceq1	$⊢ u = A \to [u] R = [A] R$
7		eceq1	$⊢ v = B \to [v] R = [B] R$
8	6 7	eqeqan12d	$⊢ (u = A \land v = B) \to ([u] R = [v] R \leftrightarrow [A] R = [B] R)$
9		eqeq12	$⊢ (u = A \land v = B) \to (u = v \leftrightarrow A = B)$
10	8 9	imbi12d	$⊢ (u = A \land v = B) \to (([u] R = [v] R \to u = v) \leftrightarrow ([A] R = [B] R \to A = B))$
11	5 10	imbi12d	$⊢ (u = A \land v = B) \to (((u \in dom R \land v \in dom R) \to ([u] R = [v] R \to u = v)) \leftrightarrow ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \to A = B)))$
12		disjimeceqim	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v)$
13		rsp2	$⊢ \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v) \to ((u \in dom R \land v \in dom R) \to ([u] R = [v] R \to u = v))$
14	12 13	syl	$⊢ Disj R \to ((u \in dom R \land v \in dom R) \to ([u] R = [v] R \to u = v))$
15	14	adantr	$⊢ (Disj R \land (A \in dom R \land B \in dom R)) \to ((u \in dom R \land v \in dom R) \to ([u] R = [v] R \to u = v))$
16	1 2 11 15	vtocl2d	$⊢ (Disj R \land (A \in dom R \land B \in dom R)) \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \to A = B))$
17	16	ex	$⊢ Disj R \to ((A \in dom R \land B \in dom R) \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \to A = B)))$
18	17	pm2.43d	$⊢ Disj R \to ((A \in dom R \land B \in dom R) \to ([A] R = [B] R \to A = B))$