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

Theorem nbrne2 4470
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

Proof of Theorem nbrne2
StepHypRef Expression
1 breq1 4455 . . . 4
21biimpcd 224 . . 3
32necon3bd 2669 . 2
43imp 429 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  =/=wne 2652   class class class wbr 4452
This theorem is referenced by:  frfi  7785  hl2at  35129  2atjm  35169  atbtwn  35170  atbtwnexOLDN  35171  atbtwnex  35172  dalem21  35418  dalem23  35420  dalem27  35423  dalem54  35450  2llnma1b  35510  lhpexle1lem  35731  lhpexle3lem  35735  lhp2at0nle  35759  4atexlemunv  35790  4atexlemnclw  35794  4atexlemcnd  35796  cdlemc5  35920  cdleme0b  35937  cdleme0c  35938  cdleme0fN  35943  cdleme01N  35946  cdleme0ex2N  35949  cdleme3b  35954  cdleme3c  35955  cdleme3g  35959  cdleme3h  35960  cdleme7aa  35967  cdleme7b  35969  cdleme7c  35970  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme11fN  35989  cdlemesner  36021  cdlemednpq  36024  cdleme19a  36029  cdleme19c  36031  cdleme21c  36053  cdleme21ct  36055  cdleme22cN  36068  cdleme22f2  36073  cdleme22g  36074  cdleme41sn3aw  36200  cdlemeg46rgv  36254  cdlemeg46req  36255  cdlemf1  36287  cdlemg27b  36422  cdlemg33b0  36427  cdlemg33c0  36428  cdlemh  36543  cdlemk14  36580  dia2dimlem1  36791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator