![]() |
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 4333 | . . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴) | |
2 | 1 | eqcomd 2777 | . . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵) |
3 | 2 | necon3ai 2968 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴}) |
4 | disjsn 4383 | . 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴}) | |
5 | 3, 4 | sylibr 224 | 1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 ∩ cin 3722 ∅c0 4063 {csn 4316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-v 3353 df-dif 3726 df-in 3730 df-nul 4064 df-sn 4317 |
This theorem is referenced by: disjpr2 4385 disjtpsn 4387 difprsn1 4466 otsndisj 5112 xpsndisj 5698 funprg 6083 funtp 6086 funcnvpr 6091 f1oprg 6322 phplem1 8295 djuin 8944 pm54.43 9026 pr2nelem 9027 f1oun2prg 13871 s3sndisj 13916 sumpr 14685 cshwsdisj 16012 setsfun0 16101 setscom 16110 xpsc0 16428 xpsc1 16429 dmdprdpr 18656 dprdpr 18657 ablfac1eulem 18679 cnfldfun 19973 m2detleib 20655 dishaus 21407 dissnlocfin 21553 xpstopnlem1 21833 perfectlem2 25176 prodpr 29912 esumpr 30468 esum2dlem 30494 prodfzo03 31021 onint1 32785 bj-disjsn01 33269 poimirlem26 33768 sumpair 39716 perfectALTVlem2 42159 gsumpr 42667 |
Copyright terms: Public domain | W3C validator |