Theorem nbrne2 4864

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 4847	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 240	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2992	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 395	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1637   ≠ wne 2978   class class class wbr 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845

This theorem is referenced by:  frfi  8440  hl2at  35183  2atjm  35223  atbtwn  35224  atbtwnexOLDN  35225  atbtwnex  35226  dalem21  35472  dalem23  35474  dalem27  35477  dalem54  35504  2llnma1b  35564  lhpexle1lem  35785  lhpexle3lem  35789  lhp2at0nle  35813  4atexlemunv  35844  4atexlemnclw  35848  4atexlemcnd  35850  cdlemc5  35973  cdleme0b  35990  cdleme0c  35991  cdleme0fN  35996  cdleme01N  35999  cdleme0ex2N  36002  cdleme3b  36007  cdleme3c  36008  cdleme3g  36012  cdleme3h  36013  cdleme7aa  36020  cdleme7b  36022  cdleme7c  36023  cdleme7d  36024  cdleme7e  36025  cdleme7ga  36026  cdleme11fN  36042  cdlemesner  36074  cdlemednpq  36077  cdleme19a  36081  cdleme19c  36083  cdleme21c  36105  cdleme21ct  36107  cdleme22cN  36120  cdleme22f2  36125  cdleme22g  36126  cdleme41sn3aw  36252  cdlemeg46rgv  36306  cdlemeg46req  36307  cdlemf1  36339  cdlemg27b  36474  cdlemg33b0  36479  cdlemg33c0  36480  cdlemh  36595  cdlemk14  36632  dia2dimlem1  36842