Theorem nbrne2 5125

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  frfi  9276  ablsimpgfindlem1  20323  ablsimpgfindlem2  20324  hl2at  40462  2atjm  40502  atbtwn  40503  atbtwnexOLDN  40504  atbtwnex  40505  dalem21  40751  dalem23  40753  dalem27  40756  dalem54  40783  2llnma1b  40843  lhpexle1lem  41064  lhpexle3lem  41068  lhp2at0nle  41092  4atexlemunv  41123  4atexlemnclw  41127  4atexlemcnd  41129  cdlemc5  41252  cdleme0b  41269  cdleme0c  41270  cdleme0fN  41275  cdleme01N  41278  cdleme0ex2N  41281  cdleme3b  41286  cdleme3c  41287  cdleme3g  41291  cdleme3h  41292  cdleme7aa  41299  cdleme7b  41301  cdleme7c  41302  cdleme7d  41303  cdleme7e  41304  cdleme7ga  41305  cdleme11fN  41321  cdlemesner  41353  cdlemednpq  41356  cdleme19a  41360  cdleme19c  41362  cdleme21c  41384  cdleme21ct  41386  cdleme22cN  41399  cdleme22f2  41404  cdleme22g  41405  cdleme41sn3aw  41531  cdlemeg46rgv  41585  cdlemeg46req  41586  cdlemf1  41618  cdlemg27b  41753  cdlemg33b0  41758  cdlemg33c0  41759  cdlemh  41874  cdlemk14  41911  dia2dimlem1  42121