Theorem nbrne2 5167

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   = wceq 1539   ≠ wne 2938   class class class wbr 5147

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  frfi  9290  ablsimpgfindlem1  20018  ablsimpgfindlem2  20019  hl2at  38579  2atjm  38619  atbtwn  38620  atbtwnexOLDN  38621  atbtwnex  38622  dalem21  38868  dalem23  38870  dalem27  38873  dalem54  38900  2llnma1b  38960  lhpexle1lem  39181  lhpexle3lem  39185  lhp2at0nle  39209  4atexlemunv  39240  4atexlemnclw  39244  4atexlemcnd  39246  cdlemc5  39369  cdleme0b  39386  cdleme0c  39387  cdleme0fN  39392  cdleme01N  39395  cdleme0ex2N  39398  cdleme3b  39403  cdleme3c  39404  cdleme3g  39408  cdleme3h  39409  cdleme7aa  39416  cdleme7b  39418  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme11fN  39438  cdlemesner  39470  cdlemednpq  39473  cdleme19a  39477  cdleme19c  39479  cdleme21c  39501  cdleme21ct  39503  cdleme22cN  39516  cdleme22f2  39521  cdleme22g  39522  cdleme41sn3aw  39648  cdlemeg46rgv  39702  cdlemeg46req  39703  cdlemf1  39735  cdlemg27b  39870  cdlemg33b0  39875  cdlemg33c0  39876  cdlemh  39991  cdlemk14  40028  dia2dimlem1  40238