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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2926   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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  frfi  9239  ablsimpgfindlem1  20046  ablsimpgfindlem2  20047  hl2at  39406  2atjm  39446  atbtwn  39447  atbtwnexOLDN  39448  atbtwnex  39449  dalem21  39695  dalem23  39697  dalem27  39700  dalem54  39727  2llnma1b  39787  lhpexle1lem  40008  lhpexle3lem  40012  lhp2at0nle  40036  4atexlemunv  40067  4atexlemnclw  40071  4atexlemcnd  40073  cdlemc5  40196  cdleme0b  40213  cdleme0c  40214  cdleme0fN  40219  cdleme01N  40222  cdleme0ex2N  40225  cdleme3b  40230  cdleme3c  40231  cdleme3g  40235  cdleme3h  40236  cdleme7aa  40243  cdleme7b  40245  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme11fN  40265  cdlemesner  40297  cdlemednpq  40300  cdleme19a  40304  cdleme19c  40306  cdleme21c  40328  cdleme21ct  40330  cdleme22cN  40343  cdleme22f2  40348  cdleme22g  40349  cdleme41sn3aw  40475  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemf1  40562  cdlemg27b  40697  cdlemg33b0  40702  cdlemg33c0  40703  cdlemh  40818  cdlemk14  40855  dia2dimlem1  41065