![]() |
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 4650 | . . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴) | |
2 | 1 | eqcomd 2732 | . . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵) |
3 | 2 | necon3ai 2955 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴}) |
4 | disjsn 4720 | . 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴}) | |
5 | 3, 4 | sylibr 233 | 1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1534 ∈ wcel 2099 ≠ wne 2930 ∩ cin 3946 ∅c0 4325 {csn 4633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-ral 3052 df-v 3464 df-dif 3950 df-in 3954 df-nul 4326 df-sn 4634 |
This theorem is referenced by: disjpr2 4722 disjtpsn 4724 difprsn1 4809 otsndisj 5527 xpsndisj 6176 funprg 6615 funtp 6618 funcnvpr 6623 f1oprg 6890 xp01disjl 8524 enpr2dOLD 9090 phplem1OLD 9253 djuin 9963 pm54.43 10046 pr2nelemOLD 10048 f1oun2prg 14928 s3sndisj 14974 sumpr 15754 cshwsdisj 17103 setsfun0 17176 setscom 17184 gsumpr 19955 dmdprdpr 20051 dprdpr 20052 ablfac1eulem 20074 cnfldfunALT 21360 cnfldfunALTOLD 21373 cnfldfunALTOLDOLD 21374 m2detleib 22627 dishaus 23380 dissnlocfin 23527 xpstopnlem1 23807 perfectlem2 27262 cosnopne 32608 prodpr 32729 esumpr 33901 esum2dlem 33927 prodfzo03 34451 onint1 36163 bj-disjsn01 36661 lindsadd 37316 poimirlem26 37349 sumpair 44652 perfectALTVlem2 47312 |
Copyright terms: Public domain | W3C validator |