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

Theorem nbrne2 5169
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 5152 . . . 4 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
21biimpcd 248 . . 3 (𝐴𝑅𝐶 → (𝐴 = 𝐵𝐵𝑅𝐶))
32necon3bd 2943 . 2 (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶𝐴𝐵))
43imp 405 1 ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1533  wne 2929   class class class wbr 5149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150
This theorem is referenced by:  frfi  9316  ablsimpgfindlem1  20081  ablsimpgfindlem2  20082  hl2at  39010  2atjm  39050  atbtwn  39051  atbtwnexOLDN  39052  atbtwnex  39053  dalem21  39299  dalem23  39301  dalem27  39304  dalem54  39331  2llnma1b  39391  lhpexle1lem  39612  lhpexle3lem  39616  lhp2at0nle  39640  4atexlemunv  39671  4atexlemnclw  39675  4atexlemcnd  39677  cdlemc5  39800  cdleme0b  39817  cdleme0c  39818  cdleme0fN  39823  cdleme01N  39826  cdleme0ex2N  39829  cdleme3b  39834  cdleme3c  39835  cdleme3g  39839  cdleme3h  39840  cdleme7aa  39847  cdleme7b  39849  cdleme7c  39850  cdleme7d  39851  cdleme7e  39852  cdleme7ga  39853  cdleme11fN  39869  cdlemesner  39901  cdlemednpq  39904  cdleme19a  39908  cdleme19c  39910  cdleme21c  39932  cdleme21ct  39934  cdleme22cN  39947  cdleme22f2  39952  cdleme22g  39953  cdleme41sn3aw  40079  cdlemeg46rgv  40133  cdlemeg46req  40134  cdlemf1  40166  cdlemg27b  40301  cdlemg33b0  40306  cdlemg33c0  40307  cdlemh  40422  cdlemk14  40459  dia2dimlem1  40669
  Copyright terms: Public domain W3C validator