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	$$⊢\left(ARC\wedge \neg BRC\right)\to A\ne B$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢A=B\to \left(ARC\leftrightarrow BRC\right)$$
2	1	biimpcd	$$⊢ARC\to \left(A=B\to BRC\right)$$
3	2	necon3bd	$$⊢ARC\to \left(\neg BRC\to A\ne B\right)$$
4	3	imp	$$⊢\left(ARC\wedge \neg BRC\right)\to A\ne B$$