| 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 4643 | . . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴) | |
| 2 | 1 | eqcomd 2743 | . . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵) |
| 3 | 2 | necon3ai 2965 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴}) |
| 4 | disjsn 4711 | . 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴}) | |
| 5 | 3, 4 | sylibr 234 | 1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∩ cin 3950 ∅c0 4333 {csn 4626 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-v 3482 df-dif 3954 df-in 3958 df-nul 4334 df-sn 4627 |
| This theorem is referenced by: disjpr2 4713 disjtpsn 4715 difprsn1 4800 otsndisj 5524 xpsndisj 6183 funprg 6620 funtp 6623 funcnvpr 6628 f1oprg 6893 xp01disjl 8530 enpr2dOLD 9090 phplem1OLD 9254 djuin 9958 pm54.43 10041 pr2nelemOLD 10043 f1oun2prg 14956 s3sndisj 15006 sumpr 15784 cshwsdisj 17136 setsfun0 17209 setscom 17217 gsumpr 19973 dmdprdpr 20069 dprdpr 20070 ablfac1eulem 20092 cnfldfunALT 21379 cnfldfunALTOLD 21392 cnfldfunALTOLDOLD 21393 m2detleib 22637 dishaus 23390 dissnlocfin 23537 xpstopnlem1 23817 perfectlem2 27274 cosnopne 32703 prodpr 32828 esumpr 34067 esum2dlem 34093 prodfzo03 34618 onint1 36450 bj-disjsn01 36953 lindsadd 37620 poimirlem26 37653 sumpair 45040 perfectALTVlem2 47709 |
| Copyright terms: Public domain | W3C validator |