Theorem nbrne2 5125

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 5108	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 252	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2974	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 411	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1563   ≠ wne 2960   class class class wbr 5105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106

This theorem is referenced by:  frfi  9233  ablsimpgfindlem1  20170  ablsimpgfindlem2  20171  hl2at  40041  2atjm  40081  atbtwn  40082  atbtwnexOLDN  40083  atbtwnex  40084  dalem21  40330  dalem23  40332  dalem27  40335  dalem54  40362  2llnma1b  40422  lhpexle1lem  40643  lhpexle3lem  40647  lhp2at0nle  40671  4atexlemunv  40702  4atexlemnclw  40706  4atexlemcnd  40708  cdlemc5  40831  cdleme0b  40848  cdleme0c  40849  cdleme0fN  40854  cdleme01N  40857  cdleme0ex2N  40860  cdleme3b  40865  cdleme3c  40866  cdleme3g  40870  cdleme3h  40871  cdleme7aa  40878  cdleme7b  40880  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme11fN  40900  cdlemesner  40932  cdlemednpq  40935  cdleme19a  40939  cdleme19c  40941  cdleme21c  40963  cdleme21ct  40965  cdleme22cN  40978  cdleme22f2  40983  cdleme22g  40984  cdleme41sn3aw  41110  cdlemeg46rgv  41164  cdlemeg46req  41165  cdlemf1  41197  cdlemg27b  41332  cdlemg33b0  41337  cdlemg33c0  41338  cdlemh  41453  cdlemk14  41490  dia2dimlem1  41700