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 | uncom 4131 | . 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵})) | |
2 | snssi 4743 | . . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴) | |
3 | undif 4432 | . . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) | |
4 | 2, 3 | sylib 220 | . 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) |
5 | 1, 4 | syl5eq 2870 | 1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 ∖ cdif 3935 ∪ cun 3936 ⊆ wss 3938 {csn 4569 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-sn 4570 |
This theorem is referenced by: fnsnsplit 6948 fsnunf2 6950 difsnexi 7485 difsnen 8601 enfixsn 8628 phplem2 8699 pssnn 8738 dif1en 8753 frfi 8765 xpfi 8791 dif1card 9438 hashgt23el 13788 hashfun 13801 fprodfvdvdsd 15685 prmdvdsprmo 16380 mreexexlem4d 16920 symgextf1 18551 symgextfo 18552 symgfixf1 18567 gsumdifsnd 19083 gsummgp0 19360 islindf4 20984 scmatf1 21142 gsummatr01 21270 tdeglem4 24656 finsumvtxdg2sstep 27333 dfconngr1 27969 satfv1lem 32611 bj-raldifsn 34394 lindsadd 34887 lindsenlbs 34889 poimirlem25 34919 poimirlem27 34921 hdmap14lem4a 39009 hdmap14lem13 39018 supxrmnf2 41714 infxrpnf2 41746 fsumnncl 41859 hoidmv1lelem2 42881 gsumdifsndf 44095 mgpsumunsn 44416 |
Copyright terms: Public domain | W3C validator |