Metamath Proof Explorer

Theorem nbrne2

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 nbrne2 
|- ( ( A R C /\ -. B R C ) -> A =/= B )

Proof

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