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

Theorem nbrne2 4173
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 4158 . . . 4  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
21biimpcd 216 . . 3  |-  ( A R C  ->  ( A  =  B  ->  B R C ) )
32necon3bd 2589 . 2  |-  ( A R C  ->  ( -.  B R C  ->  A  =/=  B ) )
43imp 419 1  |-  ( ( A R C  /\  -.  B R C )  ->  A  =/=  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    = wceq 1649    =/= wne 2552   class class class wbr 4155
This theorem is referenced by:  frfi  7290  hl2at  29521  2atjm  29561  atbtwn  29562  atbtwnexOLDN  29563  atbtwnex  29564  dalem21  29810  dalem23  29812  dalem27  29815  dalem54  29842  2llnma1b  29902  lhpexle1lem  30123  lhpexle3lem  30127  lhp2at0nle  30151  4atexlemunv  30182  4atexlemnclw  30186  4atexlemcnd  30188  cdlemc5  30311  cdleme0b  30328  cdleme0c  30329  cdleme0fN  30334  cdleme01N  30337  cdleme0ex2N  30340  cdleme3b  30345  cdleme3c  30346  cdleme3g  30350  cdleme3h  30351  cdleme7aa  30358  cdleme7b  30360  cdleme7c  30361  cdleme7d  30362  cdleme7e  30363  cdleme7ga  30364  cdleme11fN  30380  cdlemesner  30412  cdlemednpq  30415  cdleme19a  30419  cdleme19c  30421  cdleme21c  30443  cdleme21ct  30445  cdleme22cN  30458  cdleme22f2  30463  cdleme22g  30464  cdleme41sn3aw  30590  cdlemeg46rgv  30644  cdlemeg46req  30645  cdlemf1  30677  cdlemg27b  30812  cdlemg33b0  30817  cdlemg33c0  30818  cdlemh  30933  cdlemk14  30970  dia2dimlem1  31181
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-br 4156
  Copyright terms: Public domain W3C validator