Theorem nbrne2 5163

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  frfi  9321  ablsimpgfindlem1  20127  ablsimpgfindlem2  20128  hl2at  39407  2atjm  39447  atbtwn  39448  atbtwnexOLDN  39449  atbtwnex  39450  dalem21  39696  dalem23  39698  dalem27  39701  dalem54  39728  2llnma1b  39788  lhpexle1lem  40009  lhpexle3lem  40013  lhp2at0nle  40037  4atexlemunv  40068  4atexlemnclw  40072  4atexlemcnd  40074  cdlemc5  40197  cdleme0b  40214  cdleme0c  40215  cdleme0fN  40220  cdleme01N  40223  cdleme0ex2N  40226  cdleme3b  40231  cdleme3c  40232  cdleme3g  40236  cdleme3h  40237  cdleme7aa  40244  cdleme7b  40246  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme11fN  40266  cdlemesner  40298  cdlemednpq  40301  cdleme19a  40305  cdleme19c  40307  cdleme21c  40329  cdleme21ct  40331  cdleme22cN  40344  cdleme22f2  40349  cdleme22g  40350  cdleme41sn3aw  40476  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemf1  40563  cdlemg27b  40698  cdlemg33b0  40703  cdlemg33c0  40704  cdlemh  40819  cdlemk14  40856  dia2dimlem1  41066