Theorem nbrne2 5169

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   = wceq 1533   ≠ wne 2929   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150

This theorem is referenced by:  frfi  9316  ablsimpgfindlem1  20081  ablsimpgfindlem2  20082  hl2at  39010  2atjm  39050  atbtwn  39051  atbtwnexOLDN  39052  atbtwnex  39053  dalem21  39299  dalem23  39301  dalem27  39304  dalem54  39331  2llnma1b  39391  lhpexle1lem  39612  lhpexle3lem  39616  lhp2at0nle  39640  4atexlemunv  39671  4atexlemnclw  39675  4atexlemcnd  39677  cdlemc5  39800  cdleme0b  39817  cdleme0c  39818  cdleme0fN  39823  cdleme01N  39826  cdleme0ex2N  39829  cdleme3b  39834  cdleme3c  39835  cdleme3g  39839  cdleme3h  39840  cdleme7aa  39847  cdleme7b  39849  cdleme7c  39850  cdleme7d  39851  cdleme7e  39852  cdleme7ga  39853  cdleme11fN  39869  cdlemesner  39901  cdlemednpq  39904  cdleme19a  39908  cdleme19c  39910  cdleme21c  39932  cdleme21ct  39934  cdleme22cN  39947  cdleme22f2  39952  cdleme22g  39953  cdleme41sn3aw  40079  cdlemeg46rgv  40133  cdlemeg46req  40134  cdlemf1  40166  cdlemg27b  40301  cdlemg33b0  40306  cdlemg33c0  40307  cdlemh  40422  cdlemk14  40459  dia2dimlem1  40669