Theorem nbrne2 5131

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 5112	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 252	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2972	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 411	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570   ≠ wne 2958   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  frfi  9241  ablsimpgfindlem1  20174  ablsimpgfindlem2  20175  hl2at  40199  2atjm  40239  atbtwn  40240  atbtwnexOLDN  40241  atbtwnex  40242  dalem21  40488  dalem23  40490  dalem27  40493  dalem54  40520  2llnma1b  40580  lhpexle1lem  40801  lhpexle3lem  40805  lhp2at0nle  40829  4atexlemunv  40860  4atexlemnclw  40864  4atexlemcnd  40866  cdlemc5  40989  cdleme0b  41006  cdleme0c  41007  cdleme0fN  41012  cdleme01N  41015  cdleme0ex2N  41018  cdleme3b  41023  cdleme3c  41024  cdleme3g  41028  cdleme3h  41029  cdleme7aa  41036  cdleme7b  41038  cdleme7c  41039  cdleme7d  41040  cdleme7e  41041  cdleme7ga  41042  cdleme11fN  41058  cdlemesner  41090  cdlemednpq  41093  cdleme19a  41097  cdleme19c  41099  cdleme21c  41121  cdleme21ct  41123  cdleme22cN  41136  cdleme22f2  41141  cdleme22g  41142  cdleme41sn3aw  41268  cdlemeg46rgv  41322  cdlemeg46req  41323  cdlemf1  41355  cdlemg27b  41490  cdlemg33b0  41495  cdlemg33c0  41496  cdlemh  41611  cdlemk14  41648  dia2dimlem1  41858