Theorem difsnid 4341

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	|- ( B e. A -> ( ( A \ { B } ) u. { B } ) = A )

Proof of Theorem difsnid

Step	Hyp	Ref	Expression
1		uncom 3757	. 2 |- ( ( A \ { B } ) u. { B } ) = ( { B } u. ( A \ { B } ) )
2		snssi 4339	. . 3 |- ( B e. A -> { B } C_ A )
3		undif 4049	. . 3 |- ( { B } C_ A <-> ( { B } u. ( A \ { B } ) ) = A )
4	2, 3	sylib 208	. 2 |- ( B e. A -> ( { B } u. ( A \ { B } ) ) = A )
5	1, 4	syl5eq 2668	1 |- ( B e. A -> ( ( A \ { B } ) u. { B } ) = A )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   \ cdif 3571   u. cun 3572   C_ wss 3574   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178

This theorem is referenced by:  fnsnsplit  6450  fsnunf2  6452  difsnexi  6970  difsnen  8042  enfixsn  8069  phplem2  8140  pssnn  8178  dif1en  8193  frfi  8205  xpfi  8231  dif1card  8833  hashfun  13224  fprodfvdvdsd  15058  prmdvdsprmo  15746  mreexexlem4d  16307  symgextf1  17841  symgextfo  17842  symgfixf1  17857  gsumdifsnd  18360  gsummgp0  18608  islindf4  20177  scmatf1  20337  gsummatr01  20465  tdeglem4  23820  finsumvtxdg2sstep  26445  dfconngr1  27048  bj-raldifsn  33054  lindsenlbs  33404  poimirlem25  33434  poimirlem27  33436  hdmap14lem4a  37163  hdmap14lem13  37172  supxrmnf2  39660  infxrpnf2  39693  fsumnncl  39803  hoidmv1lelem2  40806  mgpsumunsn  42140  gsumdifsndf  42144