Theorem nbrne2 5099

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1542   ≠ wne 2945   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ne 2946  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080

This theorem is referenced by:  frfi  9035  ablsimpgfindlem1  19706  ablsimpgfindlem2  19707  hl2at  37413  2atjm  37453  atbtwn  37454  atbtwnexOLDN  37455  atbtwnex  37456  dalem21  37702  dalem23  37704  dalem27  37707  dalem54  37734  2llnma1b  37794  lhpexle1lem  38015  lhpexle3lem  38019  lhp2at0nle  38043  4atexlemunv  38074  4atexlemnclw  38078  4atexlemcnd  38080  cdlemc5  38203  cdleme0b  38220  cdleme0c  38221  cdleme0fN  38226  cdleme01N  38229  cdleme0ex2N  38232  cdleme3b  38237  cdleme3c  38238  cdleme3g  38242  cdleme3h  38243  cdleme7aa  38250  cdleme7b  38252  cdleme7c  38253  cdleme7d  38254  cdleme7e  38255  cdleme7ga  38256  cdleme11fN  38272  cdlemesner  38304  cdlemednpq  38307  cdleme19a  38311  cdleme19c  38313  cdleme21c  38335  cdleme21ct  38337  cdleme22cN  38350  cdleme22f2  38355  cdleme22g  38356  cdleme41sn3aw  38482  cdlemeg46rgv  38536  cdlemeg46req  38537  cdlemf1  38569  cdlemg27b  38704  cdlemg33b0  38709  cdlemg33c0  38710  cdlemh  38825  cdlemk14  38862  dia2dimlem1  39072