Theorem nbrne2 5127

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ≠ wne 2958   class class class wbr 5105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106

This theorem is used by:  frfi  9287  ablsimpgfindlem1  20335  ablsimpgfindlem2  20336  hl2at  40602  2atjm  40642  atbtwn  40643  atbtwnexOLDN  40644  atbtwnex  40645  dalem21  40891  dalem23  40893  dalem27  40896  dalem54  40923  2llnma1b  40983  lhpexle1lem  41204  lhpexle3lem  41208  lhp2at0nle  41232  4atexlemunv  41263  4atexlemnclw  41267  4atexlemcnd  41269  cdlemc5  41392  cdleme0b  41409  cdleme0c  41410  cdleme0fN  41415  cdleme01N  41418  cdleme0ex2N  41421  cdleme3b  41426  cdleme3c  41427  cdleme3g  41431  cdleme3h  41432  cdleme7aa  41439  cdleme7b  41441  cdleme7c  41442  cdleme7d  41443  cdleme7e  41444  cdleme7ga  41445  cdleme11fN  41461  cdlemesner  41493  cdlemednpq  41496  cdleme19a  41500  cdleme19c  41502  cdleme21c  41524  cdleme21ct  41526  cdleme22cN  41539  cdleme22f2  41544  cdleme22g  41545  cdleme41sn3aw  41671  cdlemeg46rgv  41725  cdlemeg46req  41726  cdlemf1  41758  cdlemg27b  41893  cdlemg33b0  41898  cdlemg33c0  41899  cdlemh  42014  cdlemk14  42051  dia2dimlem1  42261