Theorem nbrne2 5133

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2960   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  frfi  9252  ablsimpgfindlem1  20225  ablsimpgfindlem2  20226  hl2at  40239  2atjm  40279  atbtwn  40280  atbtwnexOLDN  40281  atbtwnex  40282  dalem21  40528  dalem23  40530  dalem27  40533  dalem54  40560  2llnma1b  40620  lhpexle1lem  40841  lhpexle3lem  40845  lhp2at0nle  40869  4atexlemunv  40900  4atexlemnclw  40904  4atexlemcnd  40906  cdlemc5  41029  cdleme0b  41046  cdleme0c  41047  cdleme0fN  41052  cdleme01N  41055  cdleme0ex2N  41058  cdleme3b  41063  cdleme3c  41064  cdleme3g  41068  cdleme3h  41069  cdleme7aa  41076  cdleme7b  41078  cdleme7c  41079  cdleme7d  41080  cdleme7e  41081  cdleme7ga  41082  cdleme11fN  41098  cdlemesner  41130  cdlemednpq  41133  cdleme19a  41137  cdleme19c  41139  cdleme21c  41161  cdleme21ct  41163  cdleme22cN  41176  cdleme22f2  41181  cdleme22g  41182  cdleme41sn3aw  41308  cdlemeg46rgv  41362  cdlemeg46req  41363  cdlemf1  41395  cdlemg27b  41530  cdlemg33b0  41535  cdlemg33c0  41536  cdlemh  41651  cdlemk14  41688  dia2dimlem1  41898