|   | 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 4786 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴)) | |
| 2 | simpl 482 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝑥 ∈ 𝐵) | |
| 3 | nelelne 3041 | . . . . 5 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ≠ 𝐴)) | |
| 4 | 3 | ancld 550 | . . . 4 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴))) | 
| 5 | 2, 4 | impbid2 226 | . . 3 ⊢ (¬ 𝐴 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) ↔ 𝑥 ∈ 𝐵)) | 
| 6 | 1, 5 | bitrid 283 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥 ∈ 𝐵)) | 
| 7 | 6 | eqrdv 2735 | 1 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∖ cdif 3948 {csn 4626 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-v 3482 df-dif 3954 df-sn 4627 | 
| This theorem is referenced by: difsnb 4806 difsnexi 7781 domdifsn 9094 domunsncan 9112 frfi 9321 infdifsn 9697 dfn2 12539 hashgt23el 14463 clslp 23156 xrge00 33017 lindsadd 37620 lindsenlbs 37622 poimirlem2 37629 poimirlem4 37631 poimirlem6 37633 poimirlem7 37634 poimirlem8 37635 poimirlem19 37646 poimirlem23 37650 supxrmnf2 45444 infxrpnf2 45474 dvmptfprodlem 45959 hoiprodp1 46603 | 
| Copyright terms: Public domain | W3C validator |