Theorem nbrne2 4824

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

Step	Hyp	Ref	Expression
1		breq1 4807	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 239	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2946	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 444	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1632   ≠ wne 2932   class class class wbr 4804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805

This theorem is referenced by:  frfi  8372  hl2at  35212  2atjm  35252  atbtwn  35253  atbtwnexOLDN  35254  atbtwnex  35255  dalem21  35501  dalem23  35503  dalem27  35506  dalem54  35533  2llnma1b  35593  lhpexle1lem  35814  lhpexle3lem  35818  lhp2at0nle  35842  4atexlemunv  35873  4atexlemnclw  35877  4atexlemcnd  35879  cdlemc5  36003  cdleme0b  36020  cdleme0c  36021  cdleme0fN  36026  cdleme01N  36029  cdleme0ex2N  36032  cdleme3b  36037  cdleme3c  36038  cdleme3g  36042  cdleme3h  36043  cdleme7aa  36050  cdleme7b  36052  cdleme7c  36053  cdleme7d  36054  cdleme7e  36055  cdleme7ga  36056  cdleme11fN  36072  cdlemesner  36104  cdlemednpq  36107  cdleme19a  36111  cdleme19c  36113  cdleme21c  36135  cdleme21ct  36137  cdleme22cN  36150  cdleme22f2  36155  cdleme22g  36156  cdleme41sn3aw  36282  cdlemeg46rgv  36336  cdlemeg46req  36337  cdlemf1  36369  cdlemg27b  36504  cdlemg33b0  36509  cdlemg33c0  36510  cdlemh  36625  cdlemk14  36662  dia2dimlem1  36873