MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difsnid Structured version   Visualization version   GIF version

Theorem difsnid 4723
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.)
Assertion
Ref Expression
difsnid (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Proof of Theorem difsnid
StepHypRef Expression
1 uncom 4067 . 2 ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = ({𝐵} ∪ (𝐴 ∖ {𝐵}))
2 snssi 4721 . . 3 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
3 undif 4396 . . 3 ({𝐵} ⊆ 𝐴 ↔ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
42, 3sylib 221 . 2 (𝐵𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴)
51, 4eqtrid 2789 1 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2110  cdif 3863  cun 3864  wss 3866  {csn 4541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-sn 4542
This theorem is referenced by:  fnsnsplit  6999  fsnunf2  7001  difsnexi  7546  difsnen  8727  enfixsn  8754  phplem2  8826  pssnn  8846  pssnnOLD  8895  dif1enALT  8907  frfi  8916  xpfi  8942  dif1card  9624  hashgt23el  13991  hashfun  14004  fprodfvdvdsd  15895  prmdvdsprmo  16595  mreexexlem4d  17150  symgextf1  18813  symgextfo  18814  symgfixf1  18829  gsumdifsnd  19346  gsummgp0  19626  islindf4  20800  scmatf1  21428  gsummatr01  21556  tdeglem4  24957  tdeglem4OLD  24958  finsumvtxdg2sstep  27637  dfconngr1  28271  satfv1lem  33037  bj-raldifsn  35006  lindsadd  35507  lindsenlbs  35509  poimirlem25  35539  poimirlem27  35541  hdmap14lem4a  39622  hdmap14lem13  39631  supxrmnf2  42646  infxrpnf2  42678  fsumnncl  42788  hoidmv1lelem2  43805  gsumdifsndf  45048  mgpsumunsn  45370
  Copyright terms: Public domain W3C validator