![]() |
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 4680 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴)) | |
2 | simpl 486 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝑥 ∈ 𝐵) | |
3 | nelelne 3085 | . . . . 5 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ≠ 𝐴)) | |
4 | 3 | ancld 554 | . . . 4 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴))) |
5 | 2, 4 | impbid2 229 | . . 3 ⊢ (¬ 𝐴 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) ↔ 𝑥 ∈ 𝐵)) |
6 | 1, 5 | syl5bb 286 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥 ∈ 𝐵)) |
7 | 6 | eqrdv 2796 | 1 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∖ cdif 3878 {csn 4525 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-v 3443 df-dif 3884 df-sn 4526 |
This theorem is referenced by: difsnb 4699 difsnexi 7463 domdifsn 8583 domunsncan 8600 frfi 8747 infdifsn 9104 dfn2 11898 hashgt23el 13781 clslp 21753 xrge00 30720 lindsadd 35050 lindsenlbs 35052 poimirlem2 35059 poimirlem4 35061 poimirlem6 35063 poimirlem7 35064 poimirlem8 35065 poimirlem19 35076 poimirlem23 35080 supxrmnf2 42070 infxrpnf2 42102 dvmptfprodlem 42586 hoiprodp1 43227 |
Copyright terms: Public domain | W3C validator |