MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nbrne2 Unicode version

Theorem nbrne2 4057
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
StepHypRef Expression
1 breq1 4042 . . . 4  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
21biimpcd 215 . . 3  |-  ( A R C  ->  ( A  =  B  ->  B R C ) )
32necon3bd 2496 . 2  |-  ( A R C  ->  ( -.  B R C  ->  A  =/=  B ) )
43imp 418 1  |-  ( ( A R C  /\  -.  B R C )  ->  A  =/=  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1632    =/= wne 2459   class class class wbr 4039
This theorem is referenced by:  frfi  7118  hl2at  30216  2atjm  30256  atbtwn  30257  atbtwnexOLDN  30258  atbtwnex  30259  dalem21  30505  dalem23  30507  dalem27  30510  dalem54  30537  2llnma1b  30597  lhpexle1lem  30818  lhpexle3lem  30822  lhp2at0nle  30846  4atexlemunv  30877  4atexlemnclw  30881  4atexlemcnd  30883  cdlemc5  31006  cdleme0b  31023  cdleme0c  31024  cdleme0fN  31029  cdleme01N  31032  cdleme0ex2N  31035  cdleme3b  31040  cdleme3c  31041  cdleme3g  31045  cdleme3h  31046  cdleme7aa  31053  cdleme7b  31055  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme11fN  31075  cdlemesner  31107  cdlemednpq  31110  cdleme19a  31114  cdleme19c  31116  cdleme21c  31138  cdleme21ct  31140  cdleme22cN  31153  cdleme22f2  31158  cdleme22g  31159  cdleme41sn3aw  31285  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemf1  31372  cdlemg27b  31507  cdlemg33b0  31512  cdlemg33c0  31513  cdlemh  31628  cdlemk14  31665  dia2dimlem1  31876
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator