Theorem nbrne2 5094

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 5077	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 248	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2957	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 407	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1539   ≠ wne 2943   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  frfi  9059  ablsimpgfindlem1  19710  ablsimpgfindlem2  19711  hl2at  37419  2atjm  37459  atbtwn  37460  atbtwnexOLDN  37461  atbtwnex  37462  dalem21  37708  dalem23  37710  dalem27  37713  dalem54  37740  2llnma1b  37800  lhpexle1lem  38021  lhpexle3lem  38025  lhp2at0nle  38049  4atexlemunv  38080  4atexlemnclw  38084  4atexlemcnd  38086  cdlemc5  38209  cdleme0b  38226  cdleme0c  38227  cdleme0fN  38232  cdleme01N  38235  cdleme0ex2N  38238  cdleme3b  38243  cdleme3c  38244  cdleme3g  38248  cdleme3h  38249  cdleme7aa  38256  cdleme7b  38258  cdleme7c  38259  cdleme7d  38260  cdleme7e  38261  cdleme7ga  38262  cdleme11fN  38278  cdlemesner  38310  cdlemednpq  38313  cdleme19a  38317  cdleme19c  38319  cdleme21c  38341  cdleme21ct  38343  cdleme22cN  38356  cdleme22f2  38361  cdleme22g  38362  cdleme41sn3aw  38488  cdlemeg46rgv  38542  cdlemeg46req  38543  cdlemf1  38575  cdlemg27b  38710  cdlemg33b0  38715  cdlemg33c0  38716  cdlemh  38831  cdlemk14  38868  dia2dimlem1  39078