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

Theorem nbrne2 4633
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 4616 . . . 4 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
21biimpcd 239 . . 3 (𝐴𝑅𝐶 → (𝐴 = 𝐵𝐵𝑅𝐶))
32necon3bd 2804 . 2 (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶𝐴𝐵))
43imp 445 1 ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1480  wne 2790   class class class wbr 4613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614
This theorem is referenced by:  frfi  8149  hl2at  34171  2atjm  34211  atbtwn  34212  atbtwnexOLDN  34213  atbtwnex  34214  dalem21  34460  dalem23  34462  dalem27  34465  dalem54  34492  2llnma1b  34552  lhpexle1lem  34773  lhpexle3lem  34777  lhp2at0nle  34801  4atexlemunv  34832  4atexlemnclw  34836  4atexlemcnd  34838  cdlemc5  34962  cdleme0b  34979  cdleme0c  34980  cdleme0fN  34985  cdleme01N  34988  cdleme0ex2N  34991  cdleme3b  34996  cdleme3c  34997  cdleme3g  35001  cdleme3h  35002  cdleme7aa  35009  cdleme7b  35011  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme11fN  35031  cdlemesner  35063  cdlemednpq  35066  cdleme19a  35071  cdleme19c  35073  cdleme21c  35095  cdleme21ct  35097  cdleme22cN  35110  cdleme22f2  35115  cdleme22g  35116  cdleme41sn3aw  35242  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemf1  35329  cdlemg27b  35464  cdlemg33b0  35469  cdlemg33c0  35470  cdlemh  35585  cdlemk14  35622  dia2dimlem1  35833
  Copyright terms: Public domain W3C validator