Metamath Proof Explorer

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 R -> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R <-> u = v ) )

Proof

Step Hyp Ref Expression
1 disjimeceqim 
 |-  ( Disj R -> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> u = v ) )
2 eceq1 
 |-  ( u = v -> [ u ] R = [ v ] R )
3 2 rgen2w 
 |-  A. u e. dom R A. v e. dom R ( u = v -> [ u ] R = [ v ] R )
4 2ralbiim 
 |-  ( A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R <-> u = v ) <-> ( A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R -> u = v ) /\ A. u e. dom R A. v e. dom R ( u = v -> [ u ] R = [ v ] R ) ) )
5 1 3 4 sylanblrc 
 |-  ( Disj R -> A. u e. dom R A. v e. dom R ( [ u ] R = [ v ] R <-> u = v ) )