Theorem nbrne2 4673

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 4656	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 239	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2808	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 445	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1483   ≠ wne 2794   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  frfi  8205  hl2at  34691  2atjm  34731  atbtwn  34732  atbtwnexOLDN  34733  atbtwnex  34734  dalem21  34980  dalem23  34982  dalem27  34985  dalem54  35012  2llnma1b  35072  lhpexle1lem  35293  lhpexle3lem  35297  lhp2at0nle  35321  4atexlemunv  35352  4atexlemnclw  35356  4atexlemcnd  35358  cdlemc5  35482  cdleme0b  35499  cdleme0c  35500  cdleme0fN  35505  cdleme01N  35508  cdleme0ex2N  35511  cdleme3b  35516  cdleme3c  35517  cdleme3g  35521  cdleme3h  35522  cdleme7aa  35529  cdleme7b  35531  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme11fN  35551  cdlemesner  35583  cdlemednpq  35586  cdleme19a  35591  cdleme19c  35593  cdleme21c  35615  cdleme21ct  35617  cdleme22cN  35630  cdleme22f2  35635  cdleme22g  35636  cdleme41sn3aw  35762  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemf1  35849  cdlemg27b  35984  cdlemg33b0  35989  cdlemg33c0  35990  cdlemh  36105  cdlemk14  36142  dia2dimlem1  36353