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

Theorem nbrne2 4222
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 4207 . . . 4  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
21biimpcd 216 . . 3  |-  ( A R C  ->  ( A  =  B  ->  B R C ) )
32necon3bd 2635 . 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 1652    =/= wne 2598   class class class wbr 4204
This theorem is referenced by:  frfi  7344  hl2at  30139  2atjm  30179  atbtwn  30180  atbtwnexOLDN  30181  atbtwnex  30182  dalem21  30428  dalem23  30430  dalem27  30433  dalem54  30460  2llnma1b  30520  lhpexle1lem  30741  lhpexle3lem  30745  lhp2at0nle  30769  4atexlemunv  30800  4atexlemnclw  30804  4atexlemcnd  30806  cdlemc5  30929  cdleme0b  30946  cdleme0c  30947  cdleme0fN  30952  cdleme01N  30955  cdleme0ex2N  30958  cdleme3b  30963  cdleme3c  30964  cdleme3g  30968  cdleme3h  30969  cdleme7aa  30976  cdleme7b  30978  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme11fN  30998  cdlemesner  31030  cdlemednpq  31033  cdleme19a  31037  cdleme19c  31039  cdleme21c  31061  cdleme21ct  31063  cdleme22cN  31076  cdleme22f2  31081  cdleme22g  31082  cdleme41sn3aw  31208  cdlemeg46rgv  31262  cdlemeg46req  31263  cdlemf1  31295  cdlemg27b  31430  cdlemg33b0  31435  cdlemg33c0  31436  cdlemh  31551  cdlemk14  31588  dia2dimlem1  31799
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator