MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difss Unicode version

Theorem difss 3305
Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
difss  |-  ( A 
\  B )  C_  A

Proof of Theorem difss
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eldifi 3300 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3186 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3151    C_ wss 3154
This theorem is referenced by:  difssd  3306  difss2  3307  ssdifss  3309  disj4  3505  0dif  3527  uneqdifeq  3544  difsnpss  3760  unidif  3861  iunxdif2  3952  difexg  4164  tz7.7  4420  tfi  4646  peano5  4681  reldif  4807  cnvdif  5089  fresaun  5414  fresaunres2  5415  resdif  5496  fndmdif  5631  difxp  6155  oev  6515  oacomf1olem  6564  oelim2  6595  swoer  6690  swoord1  6691  swoord2  6692  boxcutc  6861  undom  6952  domunsncan  6964  sbthlem1  6973  sbthlem2  6974  sbthlem4  6976  sbthlem5  6977  limenpsi  7038  phplem2  7043  php  7047  php3  7049  pssnn  7083  diffi  7091  frfi  7104  fofinf1o  7139  ixpfi2  7156  elfiun  7185  marypha1lem  7188  wemapso  7268  inf3lem3  7333  infdifsn  7359  cantnflem2  7394  dfac8alem  7658  numacn  7678  acnnum  7681  acndom2  7683  inffien  7692  kmlem5  7782  infdif  7837  infdif2  7838  ackbij1lem12  7859  ackbij1lem18  7865  fictb  7873  ssfin4  7938  fin23lem7  7944  fin23lem11  7945  fin23lem26  7953  fin23lem28  7968  fin23lem29  7969  fin23lem30  7970  isf32lem8  7988  compsscnvlem  7998  isf34lem2  8001  compssiso  8002  isf34lem4  8005  enfin1ai  8012  fin1a2lem7  8034  domtriomlem  8070  axcclem  8085  zornn0g  8134  ttukey2g  8145  konigthlem  8192  fpwwe2  8267  wundif  8338  pinn  8504  niex  8507  ltsopi  8514  dmaddpi  8516  dmmulpi  8517  lerelxr  8890  mulnzcnopr  9416  dflt2  10484  expcl2lem  11117  expclzlem  11129  hashun2  11367  fsumss  12200  fsumless  12256  cvgcmpce  12278  rpnnen2lem9  12503  rpnnen2lem11  12505  ramub1lem1  13075  ramub1lem2  13076  isstruct2  13159  structcnvcnv  13161  strleun  13240  strle1  13241  mreexexlem2d  13549  frgpnabllem2  15164  dprdfeq0  15259  dprdss  15266  dprd2da  15279  dmdprdsplit2lem  15282  dpjf  15294  dpjidcl  15295  dpjlid  15298  dpjghm  15300  ablfac1b  15307  ablfac1eulem  15309  ablfac1eu  15310  isdrng2  15524  drngmcl  15527  drngid2  15530  isdrngd  15539  lbspss  15837  lspsolv  15898  lsppratlem1  15902  lsppratlem2  15903  lsppratlem3  15904  lsppratlem4  15905  lspprat  15908  islbs2  15909  islbs3  15910  lbsextlem2  15914  lbsextlem3  15915  lbsextlem4  15916  xrs1mnd  16411  xrs10  16412  xrs1cmn  16413  xrge0subm  16414  xrge0cmn  16415  cnmsubglem  16436  expghm  16452  isopn2  16771  clsval2  16789  ntrval2  16790  ntrdif  16791  clsdif  16792  ntrss  16794  cmclsopn  16801  cmntrcld  16802  discld  16828  mretopd  16831  lpsscls  16875  lpss3  16878  restntr  16914  restlp  16915  lpcls  17094  cmpcld  17131  hauscmplem  17135  2ndcsep  17187  1stccnp  17190  hausllycmp  17222  llycmpkgen2  17247  1stckgen  17251  txkgen  17348  qtopcld  17406  qtoprest  17410  qtopcmap  17412  kqdisj  17425  trfil3  17585  isufil2  17605  ufileu  17616  filufint  17617  fixufil  17619  cfinufil  17625  ufinffr  17626  ufilen  17627  fin1aufil  17629  supnfcls  17717  fclscf  17722  flimfnfcls  17725  alexsublem  17740  alexsubALTlem3  17745  cldsubg  17795  imasdsf1olem  17939  blcld  18053  recld2  18322  xrge0gsumle  18340  divcn  18374  cdivcncf  18422  evth  18459  lebnumlem1  18461  lebnumlem2  18462  lebnumlem3  18463  bcthlem2  18749  bcthlem3  18750  bcthlem5  18752  bcth3  18755  ismbl2  18888  cmmbl  18894  nulmbl  18895  nulmbl2  18896  unmbl  18897  shftmbl  18898  volinun  18905  iundisj2  18908  voliunlem1  18909  voliunlem2  18910  volsup  18915  ioombl1lem4  18920  ioombl1  18921  uniiccdif  18935  uniioombllem3  18942  uniioombllem5  18944  uniioombl  18946  uniiccmbl  18947  mbfss  19003  itg1val2  19041  itg1cl  19042  itg1ge0  19043  i1f0  19044  i1f1  19047  i1fadd  19052  i1fmul  19053  itg1addlem4  19056  itg1addlem5  19057  i1fmulc  19060  itg1mulc  19061  itg10a  19067  itg1ge0a  19068  itg1climres  19071  mbfi1fseqlem4  19075  itg2cnlem1  19118  itg2cnlem2  19119  itgss3  19171  itgioo  19172  itgsplitioo  19194  limcdif  19228  ellimc2  19229  limcnlp  19230  ellimc3  19231  limcflflem  19232  limcflf  19233  limcmo  19234  limcmpt2  19236  limcresi  19237  perfdvf  19255  dvreslem  19261  dvres2lem  19262  dvidlem  19267  dvcnp2  19271  dvaddbr  19289  dvmulbr  19290  dvcobr  19297  dvrec  19306  dvcnvlem  19325  dvexp3  19327  dveflem  19328  dvferm1  19334  dvferm2  19336  lhop1lem  19362  lhop  19365  dvcnvrelem2  19367  ftc1lem6  19390  tdeglem4  19448  deg1n0ima  19477  ig1peu  19559  ig1pdvds  19564  aacjcl  19709  taylthlem1  19754  taylthlem2  19755  ulmdvlem3  19781  abelth  19819  logcnlem5  19995  dvlog2  20002  efopnlem2  20006  cxpcn2  20088  sqrcn  20092  rlimcnp  20262  efrlim  20266  jensen  20285  amgm  20287  wilthlem2  20309  dchrelbas2  20478  chebbnd1lem1  20620  rpvmasum2  20663  dchrisum0re  20664  dchrisum0lem3  20670  dchrisum0  20671  ballotlemfelz  23051  ballotlemfp1  23052  ballotth  23098  xrge00  23313  iundisj2fi  23366  iundisj2f  23368  gsumpropd2lem  23381  pwsiga  23493  sigainb  23499  measvunilem  23542  measiun  23547  kur14lem6  23744  kur14lem7  23745  cvmscld  23806  umgrass  23873  umgraex  23877  fundmpss  24124  wfi  24209  frind  24245  wfrlem16  24273  relsset  24430  fnsingle  24460  funimage  24469  areacirclem5  24940  prl  25178  islp3  25525  islimrs4  25593  cldbnd  26255  clsun  26257  neibastop2lem  26320  fdc  26466  divrngcl  26599  isdrngo2  26600  isdrngo3  26601  ralxpmap  26772  istopclsd  26786  eldioph2lem2  26851  diophin  26863  setindtr  27128  dnnumch1  27152  dsmmfi  27215  frlmsslss2  27256  frlmlbs  27260  islinds2  27294  lindsind2  27300  lindfrn  27302  islindf4  27319  f1omvdmvd  27397  mvdco  27399  f1omvdconj  27400  pmtrfinv  27413  pmtrfb  27417  pmtrfconj  27418  symggen  27422  symggen2  27423  psgnunilem1  27427  cnmsgngrp  27447  psgnghm2  27449  cntzsdrg  27521  isdomn3  27534  deg1mhm  27537  stoweidlem28  27788  stoweidlem50  27810  stoweidlem57  27817  islsati  29257  lsatfixedN  29272  dochsnkr  31735  hdmaprnlem4tN  32118  hdmap14lem2a  32133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator