Theorem nbrne2 5116

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ≠ wne 2930   class class class wbr 5096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  frfi  9183  ablsimpgfindlem1  20036  ablsimpgfindlem2  20037  hl2at  39604  2atjm  39644  atbtwn  39645  atbtwnexOLDN  39646  atbtwnex  39647  dalem21  39893  dalem23  39895  dalem27  39898  dalem54  39925  2llnma1b  39985  lhpexle1lem  40206  lhpexle3lem  40210  lhp2at0nle  40234  4atexlemunv  40265  4atexlemnclw  40269  4atexlemcnd  40271  cdlemc5  40394  cdleme0b  40411  cdleme0c  40412  cdleme0fN  40417  cdleme01N  40420  cdleme0ex2N  40423  cdleme3b  40428  cdleme3c  40429  cdleme3g  40433  cdleme3h  40434  cdleme7aa  40441  cdleme7b  40443  cdleme7c  40444  cdleme7d  40445  cdleme7e  40446  cdleme7ga  40447  cdleme11fN  40463  cdlemesner  40495  cdlemednpq  40498  cdleme19a  40502  cdleme19c  40504  cdleme21c  40526  cdleme21ct  40528  cdleme22cN  40541  cdleme22f2  40546  cdleme22g  40547  cdleme41sn3aw  40673  cdlemeg46rgv  40727  cdlemeg46req  40728  cdlemf1  40760  cdlemg27b  40895  cdlemg33b0  40900  cdlemg33c0  40901  cdlemh  41016  cdlemk14  41053  dia2dimlem1  41263