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

Theorem nbrne2 5073
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 5056 . . . 4 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
21biimpcd 252 . . 3 (𝐴𝑅𝐶 → (𝐴 = 𝐵𝐵𝑅𝐶))
32necon3bd 3028 . 2 (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶𝐴𝐵))
43imp 410 1 ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1538  wne 3014   class class class wbr 5053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ne 3015  df-v 3482  df-un 3924  df-sn 4551  df-pr 4553  df-op 4557  df-br 5054
This theorem is referenced by:  frfi  8762  ablsimpgfindlem1  19231  ablsimpgfindlem2  19232  hl2at  36673  2atjm  36713  atbtwn  36714  atbtwnexOLDN  36715  atbtwnex  36716  dalem21  36962  dalem23  36964  dalem27  36967  dalem54  36994  2llnma1b  37054  lhpexle1lem  37275  lhpexle3lem  37279  lhp2at0nle  37303  4atexlemunv  37334  4atexlemnclw  37338  4atexlemcnd  37340  cdlemc5  37463  cdleme0b  37480  cdleme0c  37481  cdleme0fN  37486  cdleme01N  37489  cdleme0ex2N  37492  cdleme3b  37497  cdleme3c  37498  cdleme3g  37502  cdleme3h  37503  cdleme7aa  37510  cdleme7b  37512  cdleme7c  37513  cdleme7d  37514  cdleme7e  37515  cdleme7ga  37516  cdleme11fN  37532  cdlemesner  37564  cdlemednpq  37567  cdleme19a  37571  cdleme19c  37573  cdleme21c  37595  cdleme21ct  37597  cdleme22cN  37610  cdleme22f2  37615  cdleme22g  37616  cdleme41sn3aw  37742  cdlemeg46rgv  37796  cdlemeg46req  37797  cdlemf1  37829  cdlemg27b  37964  cdlemg33b0  37969  cdlemg33c0  37970  cdlemh  38085  cdlemk14  38122  dia2dimlem1  38332
  Copyright terms: Public domain W3C validator