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