This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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