Theorem nbrne2 5092

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1547   ≠ wne 2934   class class class wbr 5072

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  frfi  9185  ablsimpgfindlem1  20075  ablsimpgfindlem2  20076  hl2at  39897  2atjm  39937  atbtwn  39938  atbtwnexOLDN  39939  atbtwnex  39940  dalem21  40186  dalem23  40188  dalem27  40191  dalem54  40218  2llnma1b  40278  lhpexle1lem  40499  lhpexle3lem  40503  lhp2at0nle  40527  4atexlemunv  40558  4atexlemnclw  40562  4atexlemcnd  40564  cdlemc5  40687  cdleme0b  40704  cdleme0c  40705  cdleme0fN  40710  cdleme01N  40713  cdleme0ex2N  40716  cdleme3b  40721  cdleme3c  40722  cdleme3g  40726  cdleme3h  40727  cdleme7aa  40734  cdleme7b  40736  cdleme7c  40737  cdleme7d  40738  cdleme7e  40739  cdleme7ga  40740  cdleme11fN  40756  cdlemesner  40788  cdlemednpq  40791  cdleme19a  40795  cdleme19c  40797  cdleme21c  40819  cdleme21ct  40821  cdleme22cN  40834  cdleme22f2  40839  cdleme22g  40840  cdleme41sn3aw  40966  cdlemeg46rgv  41020  cdlemeg46req  41021  cdlemf1  41053  cdlemg27b  41188  cdlemg33b0  41193  cdlemg33c0  41194  cdlemh  41309  cdlemk14  41346  dia2dimlem1  41556