|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > difsnid | Structured version Visualization version GIF version | ||
| Description: If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006.) | 
| Ref | Expression | 
|---|---|
| difsnid | ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | snssi 4807 | . 2 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴) | |
| 2 | undifr 4482 | . 2 ⊢ ({𝐵} ⊆ 𝐴 ↔ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) | |
| 3 | 1, 2 | sylib 218 | 1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 ∖ cdif 3947 ∪ cun 3948 ⊆ wss 3950 {csn 4625 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-sn 4626 | 
| This theorem is referenced by: fnsnsplit 7205 fsnunf2 7207 difsnexi 7782 difsnen 9094 enfixsn 9122 pssnn 9209 phplem2OLD 9256 dif1ennnALT 9312 frfi 9322 xpfiOLD 9360 dif1card 10051 hashgt23el 14464 hashfun 14477 fprodfvdvdsd 16372 prmdvdsprmo 17081 mreexexlem4d 17691 symgextf1 19440 symgextfo 19441 symgfixf1 19456 gsumdifsnd 19980 gsummgp0 20316 islindf4 21859 scmatf1 22538 gsummatr01 22666 tdeglem4 26100 finsumvtxdg2sstep 29568 dfconngr1 30208 fmptunsnop 32710 satfv1lem 35368 bj-raldifsn 37102 lindsadd 37621 lindsenlbs 37623 poimirlem25 37653 poimirlem27 37655 hdmap14lem4a 41874 hdmap14lem13 41883 supxrmnf2 45449 infxrpnf2 45479 fsumnncl 45592 hoidmv1lelem2 46612 gsumdifsndf 48102 mgpsumunsn 48282 | 
| Copyright terms: Public domain | W3C validator |