Theorem 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 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ↔ 𝑢 = 𝑣 ) )

Proof

Step	Hyp	Ref	Expression
1		disjimeceqim	⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )
2		eceq1	⊢ ( 𝑢 = 𝑣 → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 )
3	2	rgen2w	⊢ ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 )
4		2ralbiim	⊢ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ↔ 𝑢 = 𝑣 ) ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ∧ ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) )
5	1 3 4	sylanblrc	⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ↔ 𝑢 = 𝑣 ) )