Theorem difsnid 4176

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

Step	Hyp	Ref	Expression
1		uncom 3647	. 2
2		snssi 4174	. . 3
3		undif 3908	. . 3
4	2, 3	sylib 196	. 2
5	1, 4	syl5eq 2510	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  \cdif 3472  u.cun 3473  C_wss 3475  {csn 4029

This theorem is referenced by:  fnsnsplit  6108  fsnunf2  6110  difsnexi  6608  difsnen  7619  enfixsn  7646  phplem2  7717  pssnn  7758  dif1enOLD  7772  dif1en  7773  frfi  7785  xpfi  7811  dif1card  8409  hashfun  12495  mreexexlem4d  15044  symgextf1  16446  symgextfo  16447  symgfixf1  16462  gsumdifsnd  16987  gsummgp0  17256  islindf4  18873  scmatf1  19033  gsummatr01  19161  tdeglem4  22458  dfconngra1  24671  fsumnncl  31572  mgpsumunsn  32951  gsumdifsndf  32955  hdmap14lem4a  37601  hdmap14lem13  37610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-sn 4030