Theorem nbrne2 5130

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 5113	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 248	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2953	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 407	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541   ≠ wne 2939   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  frfi  9239  ablsimpgfindlem1  19900  ablsimpgfindlem2  19901  hl2at  37941  2atjm  37981  atbtwn  37982  atbtwnexOLDN  37983  atbtwnex  37984  dalem21  38230  dalem23  38232  dalem27  38235  dalem54  38262  2llnma1b  38322  lhpexle1lem  38543  lhpexle3lem  38547  lhp2at0nle  38571  4atexlemunv  38602  4atexlemnclw  38606  4atexlemcnd  38608  cdlemc5  38731  cdleme0b  38748  cdleme0c  38749  cdleme0fN  38754  cdleme01N  38757  cdleme0ex2N  38760  cdleme3b  38765  cdleme3c  38766  cdleme3g  38770  cdleme3h  38771  cdleme7aa  38778  cdleme7b  38780  cdleme7c  38781  cdleme7d  38782  cdleme7e  38783  cdleme7ga  38784  cdleme11fN  38800  cdlemesner  38832  cdlemednpq  38835  cdleme19a  38839  cdleme19c  38841  cdleme21c  38863  cdleme21ct  38865  cdleme22cN  38878  cdleme22f2  38883  cdleme22g  38884  cdleme41sn3aw  39010  cdlemeg46rgv  39064  cdlemeg46req  39065  cdlemf1  39097  cdlemg27b  39232  cdlemg33b0  39237  cdlemg33c0  39238  cdlemh  39353  cdlemk14  39390  dia2dimlem1  39600