![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > disjsn2 | Structured version Visualization version GIF version |
Description: Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998.) |
Ref | Expression |
---|---|
disjsn2 | ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsni 4452 | . . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴) | |
2 | 1 | eqcomd 2778 | . . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵) |
3 | 2 | necon3ai 2986 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴}) |
4 | disjsn 4515 | . 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴}) | |
5 | 3, 4 | sylibr 226 | 1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1507 ∈ wcel 2050 ≠ wne 2961 ∩ cin 3822 ∅c0 4172 {csn 4435 |
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 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-v 3411 df-dif 3826 df-in 3830 df-nul 4173 df-sn 4436 |
This theorem is referenced by: disjpr2 4517 disjtpsn 4519 difprsn1 4601 otsndisj 5259 xpsndisj 5854 funprg 6235 funtp 6238 funcnvpr 6243 f1oprg 6482 xp01disjl 7917 phplem1 8486 djuin 9135 pm54.43 9217 pr2nelem 9218 f1oun2prg 14135 s3sndisj 14182 sumpr 14957 cshwsdisj 16282 setsfun0 16369 setscom 16377 xpsc0 16683 xpsc1 16684 gsumpr 18822 dmdprdpr 18915 dprdpr 18916 ablfac1eulem 18938 cnfldfun 20253 m2detleib 20938 dishaus 21688 dissnlocfin 21835 xpstopnlem1 22115 perfectlem2 25502 cosnopne 30183 prodpr 30289 esumpr 30969 esum2dlem 30995 prodfzo03 31522 onint1 33317 bj-disjsn01 33759 lindsadd 34326 poimirlem26 34359 enpr2d 39929 sumpair 40711 perfectALTVlem2 43255 |
Copyright terms: Public domain | W3C validator |