Theorem nbrne2 5120

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 5103	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 251	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2971	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 410	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1560   ≠ wne 2957   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  frfi  9229  ablsimpgfindlem1  20149  ablsimpgfindlem2  20150  hl2at  40029  2atjm  40069  atbtwn  40070  atbtwnexOLDN  40071  atbtwnex  40072  dalem21  40318  dalem23  40320  dalem27  40323  dalem54  40350  2llnma1b  40410  lhpexle1lem  40631  lhpexle3lem  40635  lhp2at0nle  40659  4atexlemunv  40690  4atexlemnclw  40694  4atexlemcnd  40696  cdlemc5  40819  cdleme0b  40836  cdleme0c  40837  cdleme0fN  40842  cdleme01N  40845  cdleme0ex2N  40848  cdleme3b  40853  cdleme3c  40854  cdleme3g  40858  cdleme3h  40859  cdleme7aa  40866  cdleme7b  40868  cdleme7c  40869  cdleme7d  40870  cdleme7e  40871  cdleme7ga  40872  cdleme11fN  40888  cdlemesner  40920  cdlemednpq  40923  cdleme19a  40927  cdleme19c  40929  cdleme21c  40951  cdleme21ct  40953  cdleme22cN  40966  cdleme22f2  40971  cdleme22g  40972  cdleme41sn3aw  41098  cdlemeg46rgv  41152  cdlemeg46req  41153  cdlemf1  41185  cdlemg27b  41320  cdlemg33b0  41325  cdlemg33c0  41326  cdlemh  41441  cdlemk14  41478  dia2dimlem1  41688