![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > disjsn | GIF version |
Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
Ref | Expression |
---|---|
disjsn | ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disj1 3488 | . 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵})) | |
2 | con2b 670 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴)) | |
3 | velsn 3624 | . . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) | |
4 | 3 | imbi1i 238 | . . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴)) |
5 | imnan 691 | . . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
6 | 2, 4, 5 | 3bitri 206 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴)) |
7 | 6 | albii 1481 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴)) |
8 | alnex 1510 | . . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
9 | df-clel 2185 | . . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
10 | 8, 9 | xchbinxr 684 | . 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴) |
11 | 1, 7, 10 | 3bitri 206 | 1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1362 = wceq 1364 ∃wex 1503 ∈ wcel 2160 ∩ cin 3143 ∅c0 3437 {csn 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-v 2754 df-dif 3146 df-in 3150 df-nul 3438 df-sn 3613 |
This theorem is referenced by: disjsn2 3670 ssdifsn 3735 orddisj 4563 ndmima 5023 funtpg 5286 fnunsn 5342 ressnop0 5718 ftpg 5721 fsnunf 5737 fsnunfv 5738 enpr2d 6843 phpm 6893 fiunsnnn 6909 ac6sfi 6926 unsnfi 6947 tpfidisj 6956 iunfidisj 6975 pm54.43 7219 dju1en 7242 fzpreddisj 10101 fzp1disj 10110 frecfzennn 10457 hashunsng 10819 hashxp 10838 fsumsplitsn 11450 sumtp 11454 fsumsplitsnun 11459 fsum2dlemstep 11474 fsumconst 11494 fsumabs 11505 fsumiun 11517 fprodm1 11638 fprodunsn 11644 fprod2dlemstep 11662 fprodsplitsn 11673 ennnfonelemhf1o 12464 structcnvcnv 12528 fsumcncntop 14516 |
Copyright terms: Public domain | W3C validator |