Theorem nbrne2 5118

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 5101	. . . 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 1541   ≠ wne 2932   class class class wbr 5098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  frfi  9185  ablsimpgfindlem1  20038  ablsimpgfindlem2  20039  hl2at  39675  2atjm  39715  atbtwn  39716  atbtwnexOLDN  39717  atbtwnex  39718  dalem21  39964  dalem23  39966  dalem27  39969  dalem54  39996  2llnma1b  40056  lhpexle1lem  40277  lhpexle3lem  40281  lhp2at0nle  40305  4atexlemunv  40336  4atexlemnclw  40340  4atexlemcnd  40342  cdlemc5  40465  cdleme0b  40482  cdleme0c  40483  cdleme0fN  40488  cdleme01N  40491  cdleme0ex2N  40494  cdleme3b  40499  cdleme3c  40500  cdleme3g  40504  cdleme3h  40505  cdleme7aa  40512  cdleme7b  40514  cdleme7c  40515  cdleme7d  40516  cdleme7e  40517  cdleme7ga  40518  cdleme11fN  40534  cdlemesner  40566  cdlemednpq  40569  cdleme19a  40573  cdleme19c  40575  cdleme21c  40597  cdleme21ct  40599  cdleme22cN  40612  cdleme22f2  40617  cdleme22g  40618  cdleme41sn3aw  40744  cdlemeg46rgv  40798  cdlemeg46req  40799  cdlemf1  40831  cdlemg27b  40966  cdlemg33b0  40971  cdlemg33c0  40972  cdlemh  41087  cdlemk14  41124  dia2dimlem1  41334