| 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 3175 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶})) | |
| 2 | elsng 3648 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶)) | |
| 3 | 2 | necon3bbid 2416 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶)) |
| 4 | 3 | pm5.32i 454 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
| 5 | 1, 4 | bitri 184 | 1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
| Colors of variables: wff set class |
| Syntax hints: ¬ wn 3 ∧ wa 104 ↔ wb 105 ∈ wcel 2176 ≠ wne 2376 ∖ cdif 3163 {csn 3633 |
| 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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-v 2774 df-dif 3168 df-sn 3639 |
| This theorem is referenced by: eldifsni 3762 rexdifsn 3765 difsn 3770 fnniniseg2 5705 rexsupp 5706 mpodifsnif 6040 suppssfv 6156 suppssov1 6157 dif1o 6526 fidifsnen 6969 en2eleq 7305 en2other2 7306 elni 7423 divvalap 8749 elnnne0 9311 divfnzn 9744 modfzo0difsn 10542 modsumfzodifsn 10543 hashdifpr 10967 eff2 12024 tanvalap 12052 fzo0dvdseq 12201 oddprmgt2 12489 oddprmdvds 12710 4sqlem19 12765 setsslnid 12917 grpinvnzcl 13437 lssneln0 14169 rplogbval 15450 lgsfcl2 15516 lgsval2lem 15520 lgsval3 15528 lgsmod 15536 lgsdirprm 15544 lgsne0 15548 gausslemma2dlem0f 15564 lgsquad2lem2 15592 2lgsoddprm 15623 |
| Copyright terms: Public domain | W3C validator |