Theorem difss 3530

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

Syntax hints:   \ cdif 3371   C_ wss 3374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-dif 3377  df-in 3381  df-ss 3388

This theorem is referenced by:  difssd  3531  difss2  3532  ssdifss  3534  disj4  3781  0dif  3806  uneqdifeq  3824  difsnpss  4081  unidif  4190  iunxdif2  4285  difexg  4510  reldif  4910  cnvdif  5199  difxp  5218  wfi  5370  tz7.7  5406  fresaun  5709  fresaunres2  5710  resdif  5789  fndmdif  5940  tfi  6633  peano5  6669  wfrlem16  7001  oev  7166  oelim2  7246  swoer  7341  swoord1  7342  swoord2  7343  ralxpmap  7471  boxcutc  7515  undom  7608  domunsncan  7620  sbthlem2  7631  sbthlem4  7633  sbthlem5  7634  limenpsi  7695  phplem2  7700  php  7704  php3  7706  pssnn  7738  diffi  7751  frfi  7764  fofinf1o  7800  ixpfi2  7820  elfiun  7892  marypha1lem  7895  wemapso  8014  inf3lem3  8083  infdifsn  8109  cantnflem2  8142  dfac8alem  8406  acnnum  8429  inffien  8440  kmlem5  8530  infdif  8585  infdif2  8586  ackbij1lem18  8613  fictb  8621  fin23lem7  8692  fin23lem11  8693  fin23lem28  8716  fin23lem30  8718  compsscnvlem  8746  isf34lem2  8749  compssiso  8750  isf34lem4  8753  fin1a2lem7  8782  domtriomlem  8818  axcclem  8833  zornn0g  8881  ttukey2g  8892  konigthlem  8939  pinn  9249  niex  9252  ltsopi  9259  dmaddpi  9261  dmmulpi  9262  lerelxr  9643  mulnzcnopr  10204  dflt2  11393  expcl2lem  12229  expclzlem  12241  hashun2  12507  fsumss  13729  fsumless  13794  cvgcmpce  13816  fprodss  13940  rpnnen2lem9  14213  isstruct2  15068  structcnvcnv  15070  fsets  15087  strleun  15158  strle1  15159  mreexexlem2d  15489  gsumpropd2lem  16454  symgfixf1  17016  f1omvdmvd  17022  mvdco  17024  f1omvdconj  17025  pmtrfb  17044  pmtrfconj  17045  symggen  17049  symggen2  17050  psgnunilem1  17072  frgpnabllem2  17448  dprdss  17600  dprd2da  17613  dmdprdsplit2lem  17616  dpjidcl  17629  ablfac1b  17641  ablfac1eu  17644  isdrng2  17923  drngmcl  17926  drngid2  17929  isdrngd  17938  xrs1mnd  18944  xrs10  18945  xrs1cmn  18946  xrge0subm  18947  xrge0cmn  18948  cnmsubglem  18968  expghm  19004  cnmsgngrp  19084  psgninv  19087  dsmmfi  19238  islinds2  19308  lindsind2  19314  lindfrn  19316  islindf4  19333  mdetdiaglem  19560  mdetrsca2  19566  mdetrlin2  19569  mdetralt  19570  mdetunilem5  19578  mdetunilem9  19582  maducoeval2  19602  smadiadetglem1  19633  isopn2  19984  ntrval2  20003  ntrdif  20004  clsdif  20005  ntrss  20007  cmclsopn  20014  cmntrcldOLD  20016  discld  20042  mretopd  20045  lpsscls  20094  restntr  20135  cmpcld  20354  2ndcsep  20411  1stccnp  20414  llycmpkgen2  20502  1stckgen  20506  txkgen  20604  qtopcld  20665  qtopcmap  20671  kqdisj  20684  isufil2  20860  ufileu  20871  filufint  20872  fixufil  20874  cfinufil  20880  ufilen  20882  fin1aufil  20884  supnfcls  20972  flimfnfcls  20980  alexsublem  20996  alexsubALTlem3  21001  cldsubg  21062  imasdsf1olem  21325  recld2  21769  sszcld  21772  xrge0gsumle  21788  divcn  21837  cdivcncf  21886  bcth3  22236  ismbl2  22418  cmmbl  22425  nulmbl  22426  nulmbl2  22427  unmbl  22428  voliunlem1  22440  voliunlem2  22441  ioombl1lem4  22451  ioombl1  22452  uniioombllem3  22480  mbfss  22539  itg1cl  22580  itg1ge0  22581  i1f0  22582  i1f1  22585  i1fmul  22591  itg1addlem4  22594  itg1mulc  22599  itg10a  22605  itg1ge0a  22606  itg1climres  22609  itg2cnlem1  22656  itgioo  22710  itgsplitioo  22732  limcdif  22768  ellimc2  22769  ellimc3  22771  limcflflem  22772  limcflf  22773  limcmo  22774  limcresi  22777  dvreslem  22801  dvres2lem  22802  dvidlem  22807  dvcnp2  22811  dvaddbr  22829  dvmulbr  22830  dvcobr  22837  dvrec  22846  dvcnvlem  22865  lhop1lem  22902  lhop  22905  tdeglem4  22946  deg1n0ima  22975  aacjcl  23220  taylthlem2  23266  abelth  23333  logcnlem5  23528  dvlog2  23535  efopnlem2  23539  dvcncxp1  23620  dvcnsqrt  23621  cxpcn2  23623  sqrtcn  23627  efrlim  23832  jensen  23851  amgm  23853  lgamgulmlem2  23892  lgamucov  23900  wilthlem2  23931  dchrelbas2  24102  rpvmasum2  24287  dchrisum0re  24288  dchrisum0lem3  24294  dchrisum0  24295  tgisline  24609  umgrass  24983  frgrawopreg2  25716  xrge00  28394  submatres  28579  madjusmdetlem2  28601  madjusmdetlem3  28602  qtophaus  28610  fsumcvg4  28703  gsumesum  28827  esum2dlem  28860  pwsiga  28899  sigainb  28905  carsggect  29097  omsmeas  29102  omsmeasOLD  29103  sitgclg  29122  ballotlemfelz  29270  ballotlemfp1  29271  ballotth  29317  ballotthOLD  29355  kur14lem6  29881  kur14lem7  29882  cvmscld  29943  mclsppslem  30168  fundmpss  30353  frind  30427  relsset  30599  limitssson  30622  fnsingle  30630  funimage  30639  cldbnd  30926  clsun  30928  topdifinffinlem  31657  poimirlem8  31855  poimirlem26  31873  poimirlem30  31877  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  voliunnfl  31891  cnambfre  31896  dvtan  31899  dvasin  31935  dvacos  31936  areacirclem4  31942  fdc  31981  divrngcl  32103  isdrngo2  32104  isdrngo3  32105  islsati  32472  hdmap14lem2a  35350  istopclsd  35454  diophin  35527  setindtr  35792  dnnumch1  35815  cntzsdrg  35981  isdomn3  35994  deg1mhm  35997  sumnnodd  37593  cncficcgt0  37649  cncfiooicclem1  37654  cxpcncf2  37661  dirkercncflem2  37849  fourierdlem62  37915  fourierdlem66  37919  fourierdlem68  37921  fourierdlem95  37948  etransclem24  38006  etransclem44  38026  gsumge0cl  38064  sge0fodjrnlem  38109  carageniuncllem1  38193  upgrss  38954  lindslinindimp2lem2  39845