Theorem nbrne2 5090

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539   ≠ wne 2942   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  frfi  8989  ablsimpgfindlem1  19625  ablsimpgfindlem2  19626  hl2at  37346  2atjm  37386  atbtwn  37387  atbtwnexOLDN  37388  atbtwnex  37389  dalem21  37635  dalem23  37637  dalem27  37640  dalem54  37667  2llnma1b  37727  lhpexle1lem  37948  lhpexle3lem  37952  lhp2at0nle  37976  4atexlemunv  38007  4atexlemnclw  38011  4atexlemcnd  38013  cdlemc5  38136  cdleme0b  38153  cdleme0c  38154  cdleme0fN  38159  cdleme01N  38162  cdleme0ex2N  38165  cdleme3b  38170  cdleme3c  38171  cdleme3g  38175  cdleme3h  38176  cdleme7aa  38183  cdleme7b  38185  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme11fN  38205  cdlemesner  38237  cdlemednpq  38240  cdleme19a  38244  cdleme19c  38246  cdleme21c  38268  cdleme21ct  38270  cdleme22cN  38283  cdleme22f2  38288  cdleme22g  38289  cdleme41sn3aw  38415  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemf1  38502  cdlemg27b  38637  cdlemg33b0  38642  cdlemg33c0  38643  cdlemh  38758  cdlemk14  38795  dia2dimlem1  39005