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 4574 | . . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴) | |
2 | 1 | eqcomd 2824 | . . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵) |
3 | 2 | necon3ai 3038 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴}) |
4 | disjsn 4639 | . 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴}) | |
5 | 3, 4 | sylibr 235 | 1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ∈ wcel 2105 ≠ wne 3013 ∩ cin 3932 ∅c0 4288 {csn 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-v 3494 df-dif 3936 df-in 3940 df-nul 4289 df-sn 4558 |
This theorem is referenced by: disjpr2 4641 disjtpsn 4643 difprsn1 4725 otsndisj 5400 xpsndisj 6013 funprg 6401 funtp 6404 funcnvpr 6409 f1oprg 6652 xp01disjl 8110 enpr2d 8585 phplem1 8684 djuin 9335 pm54.43 9417 pr2nelem 9418 f1oun2prg 14267 s3sndisj 14315 sumpr 15091 cshwsdisj 16420 setsfun0 16507 setscom 16515 gsumpr 19004 dmdprdpr 19100 dprdpr 19101 ablfac1eulem 19123 cnfldfun 20485 m2detleib 21168 dishaus 21918 dissnlocfin 22065 xpstopnlem1 22345 perfectlem2 25733 cosnopne 30356 prodpr 30469 esumpr 31224 esum2dlem 31250 prodfzo03 31773 onint1 33694 bj-disjsn01 34161 lindsadd 34766 poimirlem26 34799 sumpair 41169 perfectALTVlem2 43764 |
Copyright terms: Public domain | W3C validator |