![]() |
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 4149 | . 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵})) | |
2 | snssi 4804 | . . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴) | |
3 | undif 4477 | . . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) | |
4 | 2, 3 | sylib 217 | . 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) |
5 | 1, 4 | eqtrid 2783 | 1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 ∖ cdif 3941 ∪ cun 3942 ⊆ wss 3944 {csn 4622 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-sn 4623 |
This theorem is referenced by: fnsnsplit 7166 fsnunf2 7168 difsnexi 7731 difsnen 9036 enfixsn 9064 pssnn 9151 phplem2OLD 9201 pssnnOLD 9248 dif1ennnALT 9260 frfi 9271 xpfiOLD 9301 dif1card 9987 hashgt23el 14366 hashfun 14379 fprodfvdvdsd 16259 prmdvdsprmo 16957 mreexexlem4d 17573 symgextf1 19253 symgextfo 19254 symgfixf1 19269 gsumdifsnd 19788 gsummgp0 20085 islindf4 21326 scmatf1 21962 gsummatr01 22090 tdeglem4 25506 tdeglem4OLD 25507 finsumvtxdg2sstep 28671 dfconngr1 29306 satfv1lem 34182 bj-raldifsn 35783 lindsadd 36283 lindsenlbs 36285 poimirlem25 36315 poimirlem27 36317 hdmap14lem4a 40545 hdmap14lem13 40554 supxrmnf2 43914 infxrpnf2 43944 fsumnncl 44059 hoidmv1lelem2 45079 gsumdifsndf 46361 mgpsumunsn 46683 |
Copyright terms: Public domain | W3C validator |