![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > disjsn2 | GIF version |
Description: Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.) |
Ref | Expression |
---|---|
disjsn2 | ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsni 3492 | . . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴) | |
2 | 1 | eqcomd 2105 | . . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵) |
3 | 2 | necon3ai 2316 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴}) |
4 | disjsn 3532 | . 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴}) | |
5 | 3, 4 | sylibr 133 | 1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1299 ∈ wcel 1448 ≠ wne 2267 ∩ cin 3020 ∅c0 3310 {csn 3474 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-ral 2380 df-v 2643 df-dif 3023 df-in 3027 df-nul 3311 df-sn 3480 |
This theorem is referenced by: disjpr2 3534 difprsn1 3606 diftpsn3 3608 xpsndisj 4901 funprg 5109 funtp 5112 f1oprg 5343 xp01disjl 6261 phplem1 6675 prfidisj 6744 djuinr 6863 pm54.43 6957 pr2nelem 6958 sumpr 11021 setsfun0 11777 setscom 11781 |
Copyright terms: Public domain | W3C validator |