![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nbrne2 | Structured version Visualization version GIF version |
Description: Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
Ref | Expression |
---|---|
nbrne2 | ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 4932 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
2 | 1 | biimpcd 241 | . . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶)) |
3 | 2 | necon3bd 2981 | . 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵)) |
4 | 3 | imp 398 | 1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 = wceq 1507 ≠ wne 2967 class class class wbr 4929 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 |
This theorem is referenced by: frfi 8558 hl2at 35992 2atjm 36032 atbtwn 36033 atbtwnexOLDN 36034 atbtwnex 36035 dalem21 36281 dalem23 36283 dalem27 36286 dalem54 36313 2llnma1b 36373 lhpexle1lem 36594 lhpexle3lem 36598 lhp2at0nle 36622 4atexlemunv 36653 4atexlemnclw 36657 4atexlemcnd 36659 cdlemc5 36782 cdleme0b 36799 cdleme0c 36800 cdleme0fN 36805 cdleme01N 36808 cdleme0ex2N 36811 cdleme3b 36816 cdleme3c 36817 cdleme3g 36821 cdleme3h 36822 cdleme7aa 36829 cdleme7b 36831 cdleme7c 36832 cdleme7d 36833 cdleme7e 36834 cdleme7ga 36835 cdleme11fN 36851 cdlemesner 36883 cdlemednpq 36886 cdleme19a 36890 cdleme19c 36892 cdleme21c 36914 cdleme21ct 36916 cdleme22cN 36929 cdleme22f2 36934 cdleme22g 36935 cdleme41sn3aw 37061 cdlemeg46rgv 37115 cdlemeg46req 37116 cdlemf1 37148 cdlemg27b 37283 cdlemg33b0 37288 cdlemg33c0 37289 cdlemh 37404 cdlemk14 37441 dia2dimlem1 37651 ablsimpgfindlem1 40049 ablsimpgfindlem2 40050 |
Copyright terms: Public domain | W3C validator |