Theorem difss 3572

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.

Step	Hyp	Ref	Expression
1		eldifi 3567	. 2 |- ( x e. ( A \ B ) -> x e. A )
2	1	ssriv 3448	1 |- ( A \ B ) C_ A

Syntax hints:   \ cdif 3413   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-dif 3419  df-in 3423  df-ss 3430

This theorem is referenced by:  difssd  3573  difss2  3574  ssdifss  3576  disj4  3825  0dif  3850  uneqdifeq  3868  difsnpss  4128  unidif  4245  iunxdif2  4340  difexg  4565  reldif  4972  cnvdif  5261  difxp  5280  wfi  5432  tz7.7  5468  fresaun  5777  fresaunres2  5778  resdif  5857  fndmdif  6009  tfi  6707  peano5  6743  wfrlem16  7077  oev  7242  oelim2  7322  swoer  7417  swoord1  7418  swoord2  7419  ralxpmap  7547  boxcutc  7591  undom  7686  domunsncan  7698  sbthlem2  7709  sbthlem4  7711  sbthlem5  7712  limenpsi  7773  phplem2  7778  php  7782  php3  7784  pssnn  7816  diffi  7829  frfi  7842  fofinf1o  7878  ixpfi2  7898  elfiun  7970  marypha1lem  7973  wemapso  8092  inf3lem3  8161  infdifsn  8188  cantnflem2  8221  dfac8alem  8486  acnnum  8509  inffien  8520  kmlem5  8610  infdif  8665  infdif2  8666  ackbij1lem18  8693  fictb  8701  fin23lem7  8772  fin23lem11  8773  fin23lem28  8796  fin23lem30  8798  compsscnvlem  8826  isf34lem2  8829  compssiso  8830  isf34lem4  8833  fin1a2lem7  8862  domtriomlem  8898  axcclem  8913  zornn0g  8961  ttukey2g  8972  konigthlem  9019  pinn  9329  niex  9332  ltsopi  9339  dmaddpi  9341  dmmulpi  9342  lerelxr  9723  mulnzcnopr  10286  dflt2  11476  expcl2lem  12316  expclzlem  12328  hashun2  12594  fsumss  13840  fsumless  13905  cvgcmpce  13927  fprodss  14051  rpnnen2lem9  14324  isstruct2  15179  structcnvcnv  15181  fsets  15198  strleun  15269  strle1  15270  mreexexlem2d  15600  gsumpropd2lem  16565  symgfixf1  17127  f1omvdmvd  17133  mvdco  17135  f1omvdconj  17136  pmtrfb  17155  pmtrfconj  17156  symggen  17160  symggen2  17161  psgnunilem1  17183  frgpnabllem2  17559  dprdss  17711  dprd2da  17724  dmdprdsplit2lem  17727  dpjidcl  17740  ablfac1b  17752  ablfac1eu  17755  isdrng2  18034  drngmcl  18037  drngid2  18040  isdrngd  18049  xrs1mnd  19055  xrs10  19056  xrs1cmn  19057  xrge0subm  19058  xrge0cmn  19059  cnmsubglem  19079  expghm  19116  cnmsgngrp  19196  psgninv  19199  dsmmfi  19350  islinds2  19420  lindsind2  19426  lindfrn  19428  islindf4  19445  mdetdiaglem  19672  mdetrsca2  19678  mdetrlin2  19681  mdetralt  19682  mdetunilem5  19690  mdetunilem9  19694  maducoeval2  19714  smadiadetglem1  19745  isopn2  20096  ntrval2  20115  ntrdif  20116  clsdif  20117  ntrss  20119  cmclsopn  20126  cmntrcldOLD  20128  discld  20154  mretopd  20157  lpsscls  20206  restntr  20247  cmpcld  20466  2ndcsep  20523  1stccnp  20526  llycmpkgen2  20614  1stckgen  20618  txkgen  20716  qtopcld  20777  qtopcmap  20783  kqdisj  20796  isufil2  20972  ufileu  20983  filufint  20984  fixufil  20986  cfinufil  20992  ufilen  20994  fin1aufil  20996  supnfcls  21084  flimfnfcls  21092  alexsublem  21108  alexsubALTlem3  21113  cldsubg  21174  imasdsf1olem  21437  recld2  21881  sszcld  21884  xrge0gsumle  21900  divcn  21949  cdivcncf  21998  bcth3  22348  ismbl2  22530  cmmbl  22537  nulmbl  22538  nulmbl2  22539  unmbl  22540  voliunlem1  22552  voliunlem2  22553  ioombl1lem4  22563  ioombl1  22564  uniioombllem3  22592  mbfss  22651  itg1cl  22692  itg1ge0  22693  i1f0  22694  i1f1  22697  i1fmul  22703  itg1addlem4  22706  itg1mulc  22711  itg10a  22717  itg1ge0a  22718  itg1climres  22721  itg2cnlem1  22768  itgioo  22822  itgsplitioo  22844  limcdif  22880  ellimc2  22881  ellimc3  22883  limcflflem  22884  limcflf  22885  limcmo  22886  limcresi  22889  dvreslem  22913  dvres2lem  22914  dvidlem  22919  dvcnp2  22923  dvaddbr  22941  dvmulbr  22942  dvcobr  22949  dvrec  22958  dvcnvlem  22977  lhop1lem  23014  lhop  23017  tdeglem4  23058  deg1n0ima  23087  aacjcl  23332  taylthlem2  23378  abelth  23445  logcnlem5  23640  dvlog2  23647  efopnlem2  23651  dvcncxp1  23732  dvcnsqrt  23733  cxpcn2  23735  sqrtcn  23739  efrlim  23944  jensen  23963  amgm  23965  lgamgulmlem2  24004  lgamucov  24012  wilthlem2  24043  dchrelbas2  24214  rpvmasum2  24399  dchrisum0re  24400  dchrisum0lem3  24406  dchrisum0  24407  tgisline  24721  umgrass  25095  frgrawopreg2  25828  xrge00  28497  submatres  28681  madjusmdetlem2  28703  madjusmdetlem3  28704  qtophaus  28712  fsumcvg4  28805  gsumesum  28929  esum2dlem  28962  pwsiga  29001  sigainb  29007  carsggect  29199  omsmeas  29204  omsmeasOLD  29205  sitgclg  29224  ballotlemfelz  29372  ballotlemfp1  29373  ballotth  29419  ballotthOLD  29457  kur14lem6  29983  kur14lem7  29984  cvmscld  30045  mclsppslem  30270  fundmpss  30456  frind  30530  relsset  30704  limitssson  30727  fnsingle  30735  funimage  30744  cldbnd  31031  clsun  31033  topdifinffinlem  31795  poimirlem8  31993  poimirlem26  32011  poimirlem30  32015  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  voliunnfl  32029  cnambfre  32034  dvtan  32037  dvasin  32073  dvacos  32074  areacirclem4  32080  fdc  32119  divrngcl  32241  isdrngo2  32242  isdrngo3  32243  islsati  32605  hdmap14lem2a  35483  istopclsd  35587  diophin  35660  setindtr  35924  dnnumch1  35947  cntzsdrg  36113  isdomn3  36126  deg1mhm  36129  sumnnodd  37748  cncficcgt0  37804  cncfiooicclem1  37809  cxpcncf2  37816  dirkercncflem2  38004  fourierdlem62  38070  fourierdlem66  38074  fourierdlem68  38076  fourierdlem95  38103  etransclem24  38161  etransclem44  38181  gsumge0cl  38251  sge0fodjrnlem  38296  carageniuncllem1  38380  upgrss  39227  lindslinindimp2lem2  40525