Theorem nbrne2 5109

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 5092	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2	1	biimpcd 249	. . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶))
3	2	necon3bd 2940	. 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 406	1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ≠ wne 2926   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090

This theorem is referenced by:  frfi  9164  ablsimpgfindlem1  20014  ablsimpgfindlem2  20015  hl2at  39423  2atjm  39463  atbtwn  39464  atbtwnexOLDN  39465  atbtwnex  39466  dalem21  39712  dalem23  39714  dalem27  39717  dalem54  39744  2llnma1b  39804  lhpexle1lem  40025  lhpexle3lem  40029  lhp2at0nle  40053  4atexlemunv  40084  4atexlemnclw  40088  4atexlemcnd  40090  cdlemc5  40213  cdleme0b  40230  cdleme0c  40231  cdleme0fN  40236  cdleme01N  40239  cdleme0ex2N  40242  cdleme3b  40247  cdleme3c  40248  cdleme3g  40252  cdleme3h  40253  cdleme7aa  40260  cdleme7b  40262  cdleme7c  40263  cdleme7d  40264  cdleme7e  40265  cdleme7ga  40266  cdleme11fN  40282  cdlemesner  40314  cdlemednpq  40317  cdleme19a  40321  cdleme19c  40323  cdleme21c  40345  cdleme21ct  40347  cdleme22cN  40360  cdleme22f2  40365  cdleme22g  40366  cdleme41sn3aw  40492  cdlemeg46rgv  40546  cdlemeg46req  40547  cdlemf1  40579  cdlemg27b  40714  cdlemg33b0  40719  cdlemg33c0  40720  cdlemh  40835  cdlemk14  40872  dia2dimlem1  41082