![]() |
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 4118 | . 2 ⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵})) | |
2 | snssi 4773 | . . 3 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴) | |
3 | undif 4446 | . . 3 ⊢ ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) | |
4 | 2, 3 | sylib 217 | . 2 ⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) |
5 | 1, 4 | eqtrid 2789 | 1 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ∖ cdif 3912 ∪ cun 3913 ⊆ wss 3915 {csn 4591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-sn 4592 |
This theorem is referenced by: fnsnsplit 7135 fsnunf2 7137 difsnexi 7700 difsnen 9004 enfixsn 9032 pssnn 9119 phplem2OLD 9169 pssnnOLD 9216 dif1ennnALT 9228 frfi 9239 xpfiOLD 9269 dif1card 9953 hashgt23el 14331 hashfun 14344 fprodfvdvdsd 16223 prmdvdsprmo 16921 mreexexlem4d 17534 symgextf1 19210 symgextfo 19211 symgfixf1 19226 gsumdifsnd 19745 gsummgp0 20039 islindf4 21260 scmatf1 21896 gsummatr01 22024 tdeglem4 25440 tdeglem4OLD 25441 finsumvtxdg2sstep 28539 dfconngr1 29174 satfv1lem 33996 bj-raldifsn 35600 lindsadd 36100 lindsenlbs 36102 poimirlem25 36132 poimirlem27 36134 hdmap14lem4a 40363 hdmap14lem13 40372 supxrmnf2 43742 infxrpnf2 43772 fsumnncl 43887 hoidmv1lelem2 44907 gsumdifsndf 46189 mgpsumunsn 46511 |
Copyright terms: Public domain | W3C validator |