Theorem nbrne2 4434

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 4418	. . . 4 |- ( A = B -> ( A R C <-> B R C ) )
2	1	biimpcd 232	. . 3 |- ( A R C -> ( A = B -> B R C ) )
3	2	necon3bd 2649	. 2 |- ( A R C -> ( -. B R C -> A =/= B ) )
4	3	imp 435	1 |- ( ( A R C /\ -. B R C ) -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 375   = wceq 1454   =/= wne 2632   class class class wbr 4415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416

This theorem is referenced by:  frfi  7841  hl2at  33014  2atjm  33054  atbtwn  33055  atbtwnexOLDN  33056  atbtwnex  33057  dalem21  33303  dalem23  33305  dalem27  33308  dalem54  33335  2llnma1b  33395  lhpexle1lem  33616  lhpexle3lem  33620  lhp2at0nle  33644  4atexlemunv  33675  4atexlemnclw  33679  4atexlemcnd  33681  cdlemc5  33805  cdleme0b  33822  cdleme0c  33823  cdleme0fN  33828  cdleme01N  33831  cdleme0ex2N  33834  cdleme3b  33839  cdleme3c  33840  cdleme3g  33844  cdleme3h  33845  cdleme7aa  33852  cdleme7b  33854  cdleme7c  33855  cdleme7d  33856  cdleme7e  33857  cdleme7ga  33858  cdleme11fN  33874  cdlemesner  33906  cdlemednpq  33909  cdleme19a  33914  cdleme19c  33916  cdleme21c  33938  cdleme21ct  33940  cdleme22cN  33953  cdleme22f2  33958  cdleme22g  33959  cdleme41sn3aw  34085  cdlemeg46rgv  34139  cdlemeg46req  34140  cdlemf1  34172  cdlemg27b  34307  cdlemg33b0  34312  cdlemg33c0  34313  cdlemh  34428  cdlemk14  34465  dia2dimlem1  34676