Theorem nbrne2 5127

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2925   class class class wbr 5107

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  frfi  9232  ablsimpgfindlem1  20039  ablsimpgfindlem2  20040  hl2at  39399  2atjm  39439  atbtwn  39440  atbtwnexOLDN  39441  atbtwnex  39442  dalem21  39688  dalem23  39690  dalem27  39693  dalem54  39720  2llnma1b  39780  lhpexle1lem  40001  lhpexle3lem  40005  lhp2at0nle  40029  4atexlemunv  40060  4atexlemnclw  40064  4atexlemcnd  40066  cdlemc5  40189  cdleme0b  40206  cdleme0c  40207  cdleme0fN  40212  cdleme01N  40215  cdleme0ex2N  40218  cdleme3b  40223  cdleme3c  40224  cdleme3g  40228  cdleme3h  40229  cdleme7aa  40236  cdleme7b  40238  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme11fN  40258  cdlemesner  40290  cdlemednpq  40293  cdleme19a  40297  cdleme19c  40299  cdleme21c  40321  cdleme21ct  40323  cdleme22cN  40336  cdleme22f2  40341  cdleme22g  40342  cdleme41sn3aw  40468  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemf1  40555  cdlemg27b  40690  cdlemg33b0  40695  cdlemg33c0  40696  cdlemh  40811  cdlemk14  40848  dia2dimlem1  41058