Theorem nbrne2 5122

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2925   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  frfi  9208  ablsimpgfindlem1  20023  ablsimpgfindlem2  20024  hl2at  39392  2atjm  39432  atbtwn  39433  atbtwnexOLDN  39434  atbtwnex  39435  dalem21  39681  dalem23  39683  dalem27  39686  dalem54  39713  2llnma1b  39773  lhpexle1lem  39994  lhpexle3lem  39998  lhp2at0nle  40022  4atexlemunv  40053  4atexlemnclw  40057  4atexlemcnd  40059  cdlemc5  40182  cdleme0b  40199  cdleme0c  40200  cdleme0fN  40205  cdleme01N  40208  cdleme0ex2N  40211  cdleme3b  40216  cdleme3c  40217  cdleme3g  40221  cdleme3h  40222  cdleme7aa  40229  cdleme7b  40231  cdleme7c  40232  cdleme7d  40233  cdleme7e  40234  cdleme7ga  40235  cdleme11fN  40251  cdlemesner  40283  cdlemednpq  40286  cdleme19a  40290  cdleme19c  40292  cdleme21c  40314  cdleme21ct  40316  cdleme22cN  40329  cdleme22f2  40334  cdleme22g  40335  cdleme41sn3aw  40461  cdlemeg46rgv  40515  cdlemeg46req  40516  cdlemf1  40548  cdlemg27b  40683  cdlemg33b0  40688  cdlemg33c0  40689  cdlemh  40804  cdlemk14  40841  dia2dimlem1  41051