Theorem nbrne2 5139

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 5122	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 249	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2946	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 406	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2932   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  frfi  9293  ablsimpgfindlem1  20090  ablsimpgfindlem2  20091  hl2at  39424  2atjm  39464  atbtwn  39465  atbtwnexOLDN  39466  atbtwnex  39467  dalem21  39713  dalem23  39715  dalem27  39718  dalem54  39745  2llnma1b  39805  lhpexle1lem  40026  lhpexle3lem  40030  lhp2at0nle  40054  4atexlemunv  40085  4atexlemnclw  40089  4atexlemcnd  40091  cdlemc5  40214  cdleme0b  40231  cdleme0c  40232  cdleme0fN  40237  cdleme01N  40240  cdleme0ex2N  40243  cdleme3b  40248  cdleme3c  40249  cdleme3g  40253  cdleme3h  40254  cdleme7aa  40261  cdleme7b  40263  cdleme7c  40264  cdleme7d  40265  cdleme7e  40266  cdleme7ga  40267  cdleme11fN  40283  cdlemesner  40315  cdlemednpq  40318  cdleme19a  40322  cdleme19c  40324  cdleme21c  40346  cdleme21ct  40348  cdleme22cN  40361  cdleme22f2  40366  cdleme22g  40367  cdleme41sn3aw  40493  cdlemeg46rgv  40547  cdlemeg46req  40548  cdlemf1  40580  cdlemg27b  40715  cdlemg33b0  40720  cdlemg33c0  40721  cdlemh  40836  cdlemk14  40873  dia2dimlem1  41083