Theorem nbrne2 4455

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

Assertion

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

Proof of Theorem nbrne2

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   = wceq 1383   =/= wne 2638   class class class wbr 4437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438

This theorem is referenced by:  frfi  7767  hl2at  34869  2atjm  34909  atbtwn  34910  atbtwnexOLDN  34911  atbtwnex  34912  dalem21  35158  dalem23  35160  dalem27  35163  dalem54  35190  2llnma1b  35250  lhpexle1lem  35471  lhpexle3lem  35475  lhp2at0nle  35499  4atexlemunv  35530  4atexlemnclw  35534  4atexlemcnd  35536  cdlemc5  35660  cdleme0b  35677  cdleme0c  35678  cdleme0fN  35683  cdleme01N  35686  cdleme0ex2N  35689  cdleme3b  35694  cdleme3c  35695  cdleme3g  35699  cdleme3h  35700  cdleme7aa  35707  cdleme7b  35709  cdleme7c  35710  cdleme7d  35711  cdleme7e  35712  cdleme7ga  35713  cdleme11fN  35729  cdlemesner  35761  cdlemednpq  35764  cdleme19a  35769  cdleme19c  35771  cdleme21c  35793  cdleme21ct  35795  cdleme22cN  35808  cdleme22f2  35813  cdleme22g  35814  cdleme41sn3aw  35940  cdlemeg46rgv  35994  cdlemeg46req  35995  cdlemf1  36027  cdlemg27b  36162  cdlemg33b0  36167  cdlemg33c0  36168  cdlemh  36283  cdlemk14  36320  dia2dimlem1  36531