Theorem nbrne2 5072

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1537   ≠ wne 3016   class class class wbr 5052

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-rab 3147  df-v 3488  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-br 5053

This theorem is referenced by:  frfi  8749  ablsimpgfindlem1  19212  ablsimpgfindlem2  19213  hl2at  36573  2atjm  36613  atbtwn  36614  atbtwnexOLDN  36615  atbtwnex  36616  dalem21  36862  dalem23  36864  dalem27  36867  dalem54  36894  2llnma1b  36954  lhpexle1lem  37175  lhpexle3lem  37179  lhp2at0nle  37203  4atexlemunv  37234  4atexlemnclw  37238  4atexlemcnd  37240  cdlemc5  37363  cdleme0b  37380  cdleme0c  37381  cdleme0fN  37386  cdleme01N  37389  cdleme0ex2N  37392  cdleme3b  37397  cdleme3c  37398  cdleme3g  37402  cdleme3h  37403  cdleme7aa  37410  cdleme7b  37412  cdleme7c  37413  cdleme7d  37414  cdleme7e  37415  cdleme7ga  37416  cdleme11fN  37432  cdlemesner  37464  cdlemednpq  37467  cdleme19a  37471  cdleme19c  37473  cdleme21c  37495  cdleme21ct  37497  cdleme22cN  37510  cdleme22f2  37515  cdleme22g  37516  cdleme41sn3aw  37642  cdlemeg46rgv  37696  cdlemeg46req  37697  cdlemf1  37729  cdlemg27b  37864  cdlemg33b0  37869  cdlemg33c0  37870  cdlemh  37985  cdlemk14  38022  dia2dimlem1  38232