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

Theorem nbrne2 4041
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 4026 . . . 4  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
21biimpcd 215 . . 3  |-  ( A R C  ->  ( A  =  B  ->  B R C ) )
32necon3bd 2483 . 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 1623    =/= wne 2446   class class class wbr 4023
This theorem is referenced by:  frfi  7102  hl2at  29594  2atjm  29634  atbtwn  29635  atbtwnexOLDN  29636  atbtwnex  29637  dalem21  29883  dalem23  29885  dalem27  29888  dalem54  29915  2llnma1b  29975  lhpexle1lem  30196  lhpexle3lem  30200  lhp2at0nle  30224  4atexlemunv  30255  4atexlemnclw  30259  4atexlemcnd  30261  cdlemc5  30384  cdleme0b  30401  cdleme0c  30402  cdleme0fN  30407  cdleme01N  30410  cdleme0ex2N  30413  cdleme3b  30418  cdleme3c  30419  cdleme3g  30423  cdleme3h  30424  cdleme7aa  30431  cdleme7b  30433  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme11fN  30453  cdlemesner  30485  cdlemednpq  30488  cdleme19a  30492  cdleme19c  30494  cdleme21c  30516  cdleme21ct  30518  cdleme22cN  30531  cdleme22f2  30536  cdleme22g  30537  cdleme41sn3aw  30663  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemf1  30750  cdlemg27b  30885  cdlemg33b0  30890  cdlemg33c0  30891  cdlemh  31006  cdlemk14  31043  dia2dimlem1  31254
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator