Theorem nbrne2 5131

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109

This theorem is used by:  frfi  9314  ablsimpgfindlem1  20374  ablsimpgfindlem2  20375  hl2at  40728  2atjm  40768  atbtwn  40769  atbtwnexOLDN  40770  atbtwnex  40771  dalem21  41017  dalem23  41019  dalem27  41022  dalem54  41049  2llnma1b  41109  lhpexle1lem  41330  lhpexle3lem  41334  lhp2at0nle  41358  4atexlemunv  41389  4atexlemnclw  41393  4atexlemcnd  41395  cdlemc5  41518  cdleme0b  41535  cdleme0c  41536  cdleme0fN  41541  cdleme01N  41544  cdleme0ex2N  41547  cdleme3b  41552  cdleme3c  41553  cdleme3g  41557  cdleme3h  41558  cdleme7aa  41565  cdleme7b  41567  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme7ga  41571  cdleme11fN  41587  cdlemesner  41619  cdlemednpq  41622  cdleme19a  41626  cdleme19c  41628  cdleme21c  41650  cdleme21ct  41652  cdleme22cN  41665  cdleme22f2  41670  cdleme22g  41671  cdleme41sn3aw  41797  cdlemeg46rgv  41851  cdlemeg46req  41852  cdlemf1  41884  cdlemg27b  42019  cdlemg33b0  42024  cdlemg33c0  42025  cdlemh  42140  cdlemk14  42177  dia2dimlem1  42387