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 -> ( ( A e. dom R /\ B e. dom R ) -> ( [ A ] R = [ B ] R -> A = B ) ) )

Proof

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