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

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → 𝐴 ∈ dom 𝑅 )
2		simprr	⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → 𝐵 ∈ dom 𝑅 )
3		eleq1	⊢ ( 𝑢 = 𝐴 → ( 𝑢 ∈ dom 𝑅 ↔ 𝐴 ∈ dom 𝑅 ) )
4		eleq1	⊢ ( 𝑣 = 𝐵 → ( 𝑣 ∈ dom 𝑅 ↔ 𝐵 ∈ dom 𝑅 ) )
5	3 4	bi2anan9	⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ↔ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) )
6		eceq1	⊢ ( 𝑢 = 𝐴 → [ 𝑢 ] 𝑅 = [ 𝐴 ] 𝑅 )
7		eceq1	⊢ ( 𝑣 = 𝐵 → [ 𝑣 ] 𝑅 = [ 𝐵 ] 𝑅 )
8	6 7	eqeqan12d	⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
9		eqeq12	⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( 𝑢 = 𝑣 ↔ 𝐴 = 𝐵 ) )
10	8 9	imbi12d	⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ↔ ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
11	5 10	imbi12d	⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) ↔ ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
12		disjimeceqim	⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )
13		rsp2	⊢ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) )
14	12 13	syl	⊢ ( Disj 𝑅 → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) )
15	14	adantr	⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) )
16	1 2 11 15	vtocl2d	⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
17	16	ex	⊢ ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
18	17	pm2.43d	⊢ ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )