![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difsn | Structured version Visualization version GIF version |
Description: An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Ref | Expression |
---|---|
difsn | ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifsn 4791 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴)) | |
2 | simpl 482 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝑥 ∈ 𝐵) | |
3 | nelelne 3039 | . . . . 5 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ≠ 𝐴)) | |
4 | 3 | ancld 550 | . . . 4 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴))) |
5 | 2, 4 | impbid2 226 | . . 3 ⊢ (¬ 𝐴 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) ↔ 𝑥 ∈ 𝐵)) |
6 | 1, 5 | bitrid 283 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥 ∈ 𝐵)) |
7 | 6 | eqrdv 2733 | 1 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∖ cdif 3960 {csn 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-v 3480 df-dif 3966 df-sn 4632 |
This theorem is referenced by: difsnb 4811 difsnexi 7780 domdifsn 9093 domunsncan 9111 frfi 9319 infdifsn 9695 dfn2 12537 hashgt23el 14460 clslp 23172 xrge00 33000 lindsadd 37600 lindsenlbs 37602 poimirlem2 37609 poimirlem4 37611 poimirlem6 37613 poimirlem7 37614 poimirlem8 37615 poimirlem19 37626 poimirlem23 37630 supxrmnf2 45383 infxrpnf2 45413 dvmptfprodlem 45900 hoiprodp1 46544 |
Copyright terms: Public domain | W3C validator |