![]() |
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 4504 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴)) | |
2 | simpl 475 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝑥 ∈ 𝐵) | |
3 | nelelne 3067 | . . . . 5 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ≠ 𝐴)) | |
4 | 3 | ancld 547 | . . . 4 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴))) |
5 | 2, 4 | impbid2 218 | . . 3 ⊢ (¬ 𝐴 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) ↔ 𝑥 ∈ 𝐵)) |
6 | 1, 5 | syl5bb 275 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥 ∈ 𝐵)) |
7 | 6 | eqrdv 2795 | 1 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ≠ wne 2969 ∖ cdif 3764 {csn 4366 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-v 3385 df-dif 3770 df-sn 4367 |
This theorem is referenced by: difsnb 4523 difsnexi 7201 domdifsn 8283 domunsncan 8300 frfi 8445 infdifsn 8802 dfn2 11591 clslp 21278 xrge00 30194 lindsenlbs 33885 poimirlem2 33892 poimirlem4 33894 poimirlem6 33896 poimirlem7 33897 poimirlem8 33898 poimirlem19 33909 poimirlem23 33913 supxrmnf2 40391 infxrpnf2 40424 dvmptfprodlem 40891 hoiprodp1 41536 |
Copyright terms: Public domain | W3C validator |