disjimeceqbi

Description: Disj gives biconditional injectivity (domain-wise). Strengthens injectivity to an iff. (Contributed by Peter Mazsa, 3-Feb-2026)

		Ref	Expression
	Assertion	disjimeceqbi	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \leftrightarrow u = v)$

Step	Hyp	Ref	Expression
1		disjimeceqim	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v)$
2		eceq1	$⊢ u = v \to [u] R = [v] R$
3	2	rgen2w	$⊢ \forall u \in dom R \forall v \in dom R (u = v \to [u] R = [v] R)$
4		2ralbiim	$⊢ \forall u \in dom R \forall v \in dom R ([u] R = [v] R \leftrightarrow u = v) \leftrightarrow (\forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v) \land \forall u \in dom R \forall v \in dom R (u = v \to [u] R = [v] R))$
5	1 3 4	sylanblrc	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \leftrightarrow u = v)$

Metamath Proof Explorer