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

Theorem nbrne2 5077
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 5060 . . . 4 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
21biimpcd 250 . . 3 (𝐴𝑅𝐶 → (𝐴 = 𝐵𝐵𝑅𝐶))
32necon3bd 3027 . 2 (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶𝐴𝐵))
43imp 407 1 ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1528  wne 3013   class class class wbr 5057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058
This theorem is referenced by:  frfi  8751  ablsimpgfindlem1  19158  ablsimpgfindlem2  19159  hl2at  36421  2atjm  36461  atbtwn  36462  atbtwnexOLDN  36463  atbtwnex  36464  dalem21  36710  dalem23  36712  dalem27  36715  dalem54  36742  2llnma1b  36802  lhpexle1lem  37023  lhpexle3lem  37027  lhp2at0nle  37051  4atexlemunv  37082  4atexlemnclw  37086  4atexlemcnd  37088  cdlemc5  37211  cdleme0b  37228  cdleme0c  37229  cdleme0fN  37234  cdleme01N  37237  cdleme0ex2N  37240  cdleme3b  37245  cdleme3c  37246  cdleme3g  37250  cdleme3h  37251  cdleme7aa  37258  cdleme7b  37260  cdleme7c  37261  cdleme7d  37262  cdleme7e  37263  cdleme7ga  37264  cdleme11fN  37280  cdlemesner  37312  cdlemednpq  37315  cdleme19a  37319  cdleme19c  37321  cdleme21c  37343  cdleme21ct  37345  cdleme22cN  37358  cdleme22f2  37363  cdleme22g  37364  cdleme41sn3aw  37490  cdlemeg46rgv  37544  cdlemeg46req  37545  cdlemf1  37577  cdlemg27b  37712  cdlemg33b0  37717  cdlemg33c0  37718  cdlemh  37833  cdlemk14  37870  dia2dimlem1  38080
  Copyright terms: Public domain W3C validator