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

Theorem nbrne2 4427
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 4412 . . . 4
21biimpcd 224 . . 3
32necon3bd 2665 . 2
43imp 429 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1370  =/=wne 2648   class class class wbr 4409
This theorem is referenced by:  frfi  7692  hl2at  33900  2atjm  33940  atbtwn  33941  atbtwnexOLDN  33942  atbtwnex  33943  dalem21  34189  dalem23  34191  dalem27  34194  dalem54  34221  2llnma1b  34281  lhpexle1lem  34502  lhpexle3lem  34506  lhp2at0nle  34530  4atexlemunv  34561  4atexlemnclw  34565  4atexlemcnd  34567  cdlemc5  34690  cdleme0b  34707  cdleme0c  34708  cdleme0fN  34713  cdleme01N  34716  cdleme0ex2N  34719  cdleme3b  34724  cdleme3c  34725  cdleme3g  34729  cdleme3h  34730  cdleme7aa  34737  cdleme7b  34739  cdleme7c  34740  cdleme7d  34741  cdleme7e  34742  cdleme7ga  34743  cdleme11fN  34759  cdlemesner  34791  cdlemednpq  34794  cdleme19a  34798  cdleme19c  34800  cdleme21c  34822  cdleme21ct  34824  cdleme22cN  34837  cdleme22f2  34842  cdleme22g  34843  cdleme41sn3aw  34969  cdlemeg46rgv  35023  cdlemeg46req  35024  cdlemf1  35056  cdlemg27b  35191  cdlemg33b0  35196  cdlemg33c0  35197  cdlemh  35312  cdlemk14  35349  dia2dimlem1  35560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-br 4410
  Copyright terms: Public domain W3C validator