Theorem nbrne2 5050

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ≠ wne 2987   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  frfi  8747  ablsimpgfindlem1  19222  ablsimpgfindlem2  19223  hl2at  36701  2atjm  36741  atbtwn  36742  atbtwnexOLDN  36743  atbtwnex  36744  dalem21  36990  dalem23  36992  dalem27  36995  dalem54  37022  2llnma1b  37082  lhpexle1lem  37303  lhpexle3lem  37307  lhp2at0nle  37331  4atexlemunv  37362  4atexlemnclw  37366  4atexlemcnd  37368  cdlemc5  37491  cdleme0b  37508  cdleme0c  37509  cdleme0fN  37514  cdleme01N  37517  cdleme0ex2N  37520  cdleme3b  37525  cdleme3c  37526  cdleme3g  37530  cdleme3h  37531  cdleme7aa  37538  cdleme7b  37540  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme11fN  37560  cdlemesner  37592  cdlemednpq  37595  cdleme19a  37599  cdleme19c  37601  cdleme21c  37623  cdleme21ct  37625  cdleme22cN  37638  cdleme22f2  37643  cdleme22g  37644  cdleme41sn3aw  37770  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemf1  37857  cdlemg27b  37992  cdlemg33b0  37997  cdlemg33c0  37998  cdlemh  38113  cdlemk14  38150  dia2dimlem1  38360