Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eldifsn | GIF version |
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.) |
Ref | Expression |
---|---|
eldifsn | ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldif 3111 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶})) | |
2 | elsng 3575 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶)) | |
3 | 2 | necon3bbid 2367 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶)) |
4 | 3 | pm5.32i 450 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
5 | 1, 4 | bitri 183 | 1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 103 ↔ wb 104 ∈ wcel 2128 ≠ wne 2327 ∖ cdif 3099 {csn 3560 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-v 2714 df-dif 3104 df-sn 3566 |
This theorem is referenced by: eldifsni 3688 rexdifsn 3691 difsn 3693 fnniniseg2 5590 rexsupp 5591 mpodifsnif 5914 suppssfv 6028 suppssov1 6029 dif1o 6385 fidifsnen 6815 en2eleq 7130 en2other2 7131 elni 7228 divvalap 8547 elnnne0 9104 divfnzn 9530 modfzo0difsn 10294 modsumfzodifsn 10295 hashdifpr 10694 eff2 11577 tanvalap 11605 fzo0dvdseq 11748 oddprmgt2 12010 setsslnid 12241 rplogbval 13262 |
Copyright terms: Public domain | W3C validator |