Metamath Proof Explorer

Theorem nbrne1

Description: Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012)

Ref Expression
Assertion nbrne1 
|- ( ( A R B /\ -. A R C ) -> B =/= C )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( B = C -> ( A R B <-> A R C ) )
2 1 biimpcd 
 |-  ( A R B -> ( B = C -> A R C ) )
3 2 necon3bd 
 |-  ( A R B -> ( -. A R C -> B =/= C ) )
4 3 imp 
 |-  ( ( A R B /\ -. A R C ) -> B =/= C )