![]() |
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 4813 | . 2 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴) | |
2 | undifr 4489 | . 2 ⊢ ({𝐵} ⊆ 𝐴 ↔ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) | |
3 | 1, 2 | sylib 218 | 1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 ∖ cdif 3960 ∪ cun 3961 ⊆ wss 3963 {csn 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-sn 4632 |
This theorem is referenced by: fnsnsplit 7204 fsnunf2 7206 difsnexi 7780 difsnen 9092 enfixsn 9120 pssnn 9207 phplem2OLD 9253 dif1ennnALT 9309 frfi 9319 xpfiOLD 9357 dif1card 10048 hashgt23el 14460 hashfun 14473 fprodfvdvdsd 16368 prmdvdsprmo 17076 mreexexlem4d 17692 symgextf1 19454 symgextfo 19455 symgfixf1 19470 gsumdifsnd 19994 gsummgp0 20332 islindf4 21876 scmatf1 22553 gsummatr01 22681 tdeglem4 26114 finsumvtxdg2sstep 29582 dfconngr1 30217 fmptunsnop 32715 satfv1lem 35347 bj-raldifsn 37083 lindsadd 37600 lindsenlbs 37602 poimirlem25 37632 poimirlem27 37634 hdmap14lem4a 41854 hdmap14lem13 41863 supxrmnf2 45383 infxrpnf2 45413 fsumnncl 45528 hoidmv1lelem2 46548 gsumdifsndf 48025 mgpsumunsn 48206 |
Copyright terms: Public domain | W3C validator |