Theorem difss 3598

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 3593	. 2 |- ( x e. ( A \ B ) -> x e. A )
2	1	ssriv 3474	1 |- ( A \ B ) C_ A

Syntax hints:   \ cdif 3439   C_ wss 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-dif 3445  df-in 3449  df-ss 3456

This theorem is referenced by:  difssd  3599  difss2  3600  ssdifss  3602  disj4  3847  0dif  3872  uneqdifeq  3890  difsnpss  4146  unidif  4255  iunxdif2  4350  difexg  4573  reldif  4973  cnvdif  5262  difxp  5281  wfi  5432  tz7.7  5468  fresaun  5771  fresaunres2  5772  resdif  5851  fndmdif  6001  tfi  6694  peano5  6730  wfrlem16  7059  oev  7224  oelim2  7304  swoer  7399  swoord1  7400  swoord2  7401  ralxpmap  7529  boxcutc  7573  undom  7666  domunsncan  7678  sbthlem2  7689  sbthlem4  7691  sbthlem5  7692  limenpsi  7753  phplem2  7758  php  7762  php3  7764  pssnn  7796  diffi  7809  frfi  7822  fofinf1o  7858  ixpfi2  7878  elfiun  7950  marypha1lem  7953  wemapso  8066  inf3lem3  8135  infdifsn  8161  cantnflem2  8194  dfac8alem  8458  acnnum  8481  inffien  8492  kmlem5  8582  infdif  8637  infdif2  8638  ackbij1lem18  8665  fictb  8673  fin23lem7  8744  fin23lem11  8745  fin23lem28  8768  fin23lem30  8770  compsscnvlem  8798  isf34lem2  8801  compssiso  8802  isf34lem4  8805  fin1a2lem7  8834  domtriomlem  8870  axcclem  8885  zornn0g  8933  ttukey2g  8944  konigthlem  8991  pinn  9302  niex  9305  ltsopi  9312  dmaddpi  9314  dmmulpi  9315  lerelxr  9696  mulnzcnopr  10257  dflt2  11447  expcl2lem  12281  expclzlem  12293  hashun2  12559  fsumss  13769  fsumless  13834  cvgcmpce  13856  fprodss  13980  rpnnen2lem9  14253  isstruct2  15084  structcnvcnv  15086  fsets  15103  strleun  15173  strle1  15174  mreexexlem2d  15493  gsumpropd2lem  16458  symgfixf1  17020  f1omvdmvd  17026  mvdco  17028  f1omvdconj  17029  pmtrfb  17048  pmtrfconj  17049  symggen  17053  symggen2  17054  psgnunilem1  17076  frgpnabllem2  17436  dprdss  17588  dprd2da  17601  dmdprdsplit2lem  17604  dpjidcl  17617  ablfac1b  17629  ablfac1eu  17632  isdrng2  17911  drngmcl  17914  drngid2  17917  isdrngd  17926  xrs1mnd  18932  xrs10  18933  xrs1cmn  18934  xrge0subm  18935  xrge0cmn  18936  cnmsubglem  18956  expghm  18989  cnmsgngrp  19069  psgninv  19072  dsmmfi  19223  islinds2  19293  lindsind2  19299  lindfrn  19301  islindf4  19318  mdetdiaglem  19545  mdetrsca2  19551  mdetrlin2  19554  mdetralt  19555  mdetunilem5  19563  mdetunilem9  19567  maducoeval2  19587  smadiadetglem1  19618  isopn2  19969  ntrval2  19988  ntrdif  19989  clsdif  19990  ntrss  19992  cmclsopn  19999  cmntrcldOLD  20001  discld  20027  mretopd  20030  lpsscls  20079  restntr  20120  cmpcld  20339  2ndcsep  20396  1stccnp  20399  llycmpkgen2  20487  1stckgen  20491  txkgen  20589  qtopcld  20650  qtopcmap  20656  kqdisj  20669  isufil2  20845  ufileu  20856  filufint  20857  fixufil  20859  cfinufil  20865  ufilen  20867  fin1aufil  20869  supnfcls  20957  flimfnfcls  20965  alexsublem  20981  alexsubALTlem3  20986  cldsubg  21047  imasdsf1olem  21310  recld2  21734  sszcld  21737  xrge0gsumle  21753  divcn  21787  cdivcncf  21836  bcth3  22183  ismbl2  22349  cmmbl  22356  nulmbl  22357  nulmbl2  22358  unmbl  22359  voliunlem1  22371  voliunlem2  22372  ioombl1lem4  22382  ioombl1  22383  uniioombllem3  22411  mbfss  22470  itg1cl  22511  itg1ge0  22512  i1f0  22513  i1f1  22516  i1fmul  22522  itg1addlem4  22525  itg1mulc  22530  itg10a  22536  itg1ge0a  22537  itg1climres  22540  itg2cnlem1  22587  itgioo  22641  itgsplitioo  22663  limcdif  22699  ellimc2  22700  ellimc3  22702  limcflflem  22703  limcflf  22704  limcmo  22705  limcresi  22708  dvreslem  22732  dvres2lem  22733  dvidlem  22738  dvcnp2  22742  dvaddbr  22760  dvmulbr  22761  dvcobr  22768  dvrec  22777  dvcnvlem  22796  lhop1lem  22833  lhop  22836  tdeglem4  22877  deg1n0ima  22906  aacjcl  23139  taylthlem2  23185  abelth  23252  logcnlem5  23447  dvlog2  23454  efopnlem2  23458  dvcncxp1  23539  dvcnsqrt  23540  cxpcn2  23542  sqrtcn  23546  efrlim  23751  jensen  23770  amgm  23772  lgamgulmlem2  23811  lgamucov  23819  wilthlem2  23850  dchrelbas2  24019  rpvmasum2  24204  dchrisum0re  24205  dchrisum0lem3  24211  dchrisum0  24212  tgisline  24522  umgrass  24883  frgrawopreg2  25615  xrge00  28276  submatres  28462  madjusmdetlem2  28484  madjusmdetlem3  28485  qtophaus  28493  fsumcvg4  28586  gsumesum  28710  esum2dlem  28743  pwsiga  28782  sigainb  28788  carsggect  28970  omsmeas  28975  sitgclg  28994  ballotlemfelz  29140  ballotlemfp1  29141  ballotth  29187  kur14lem6  29713  kur14lem7  29714  cvmscld  29775  mclsppslem  30000  fundmpss  30185  frind  30259  relsset  30431  limitssson  30454  fnsingle  30462  funimage  30471  cldbnd  30758  clsun  30760  topdifinffinlem  31475  poimirlem8  31642  poimirlem26  31660  poimirlem30  31664  mblfinlem3  31673  mblfinlem4  31674  ismblfin  31675  voliunnfl  31678  cnambfre  31683  dvtan  31686  dvasin  31722  dvacos  31723  areacirclem4  31729  fdc  31768  divrngcl  31890  isdrngo2  31891  isdrngo3  31892  islsati  32259  hdmap14lem2a  35137  istopclsd  35241  diophin  35314  setindtr  35575  dnnumch1  35598  cntzsdrg  35757  isdomn3  35770  deg1mhm  35773  sumnnodd  37272  cncficcgt0  37328  cncfiooicclem1  37333  cxpcncf2  37340  dirkercncflem2  37525  fourierdlem62  37590  fourierdlem66  37594  fourierdlem68  37596  fourierdlem95  37623  etransclem24  37680  etransclem44  37700  gsumge0cl  37737  sge0fodjrnlem  37782  carageniuncllem1  37841  lindslinindimp2lem2  39002