Theorem difss 3626

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

Syntax hints:   \ cdif 3468   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-dif 3474  df-in 3478  df-ss 3485

This theorem is referenced by:  difssd  3627  difss2  3628  ssdifss  3630  disj4  3870  0dif  3893  uneqdifeq  3910  difsnpss  4165  unidif  4274  iunxdif2  4368  difexg  4590  tz7.7  4899  reldif  5115  cnvdif  5405  difxp  5424  fresaun  5749  fresaunres2  5750  resdif  5829  fndmdif  5978  tfi  6661  peano5  6696  oev  7156  oelim2  7236  swoer  7331  swoord1  7332  swoord2  7333  ralxpmap  7460  boxcutc  7504  undom  7597  domunsncan  7609  sbthlem2  7620  sbthlem4  7622  sbthlem5  7623  limenpsi  7684  phplem2  7689  php  7693  php3  7695  pssnn  7730  diffi  7742  frfi  7756  fofinf1o  7792  ixpfi2  7809  elfiun  7881  marypha1lem  7884  wemapso  7967  inf3lem3  8038  infdifsn  8064  cantnflem2  8100  dfac8alem  8401  acnnum  8424  inffien  8435  kmlem5  8525  infdif  8580  infdif2  8581  ackbij1lem18  8608  fictb  8616  fin23lem7  8687  fin23lem11  8688  fin23lem28  8711  fin23lem30  8713  compsscnvlem  8741  isf34lem2  8744  compssiso  8745  isf34lem4  8748  fin1a2lem7  8777  domtriomlem  8813  axcclem  8828  zornn0g  8876  ttukey2g  8887  konigthlem  8934  pinn  9247  niex  9250  ltsopi  9257  dmaddpi  9259  dmmulpi  9260  lerelxr  9641  mulnzcnopr  10186  dflt2  11345  expcl2lem  12136  expclzlem  12148  hashun2  12408  fsumss  13498  fsumless  13561  cvgcmpce  13583  rpnnen2lem9  13808  isstruct2  14490  structcnvcnv  14492  fsets  14507  strleun  14576  strle1  14577  mreexexlem2d  14891  gsumpropd2lem  15813  symgfixf1  16253  f1omvdmvd  16259  mvdco  16261  f1omvdconj  16262  pmtrfb  16281  pmtrfconj  16282  symggen  16286  symggen2  16287  psgnunilem1  16309  frgpnabllem2  16664  dprdss  16861  dprd2da  16876  dmdprdsplit2lem  16879  dpjidcl  16892  dpjidclOLD  16899  ablfac1b  16906  ablfac1eu  16909  isdrng2  17184  drngmcl  17187  drngid2  17190  isdrngd  17199  xrs1mnd  18219  xrs10  18220  xrs1cmn  18221  xrge0subm  18222  xrge0cmn  18223  cnmsubglem  18243  expghm  18291  expghmOLD  18292  cnmsgngrp  18377  psgnghm2  18379  psgninv  18380  dsmmfi  18531  islinds2  18610  lindsind2  18616  lindfrn  18618  islindf4  18635  mdetdiaglem  18862  mdetrsca2  18868  mdetrlin2  18871  mdetralt  18872  mdetunilem5  18880  mdetunilem9  18884  maducoeval2  18904  smadiadetglem1  18935  isopn2  19294  ntrval2  19313  ntrdif  19314  clsdif  19315  ntrss  19317  cmclsopn  19324  cmntrcld  19325  discld  19351  mretopd  19354  lpsscls  19403  islp3  19408  restntr  19444  cmpcld  19663  2ndcsep  19721  1stccnp  19724  llycmpkgen2  19781  1stckgen  19785  txkgen  19883  qtopcld  19944  qtopcmap  19950  kqdisj  19963  isufil2  20139  ufileu  20150  filufint  20151  fixufil  20153  cfinufil  20159  ufilen  20161  fin1aufil  20163  supnfcls  20251  flimfnfcls  20259  alexsublem  20274  alexsubALTlem3  20279  cldsubg  20339  imasdsf1olem  20606  recld2  21049  sszcld  21052  xrge0gsumle  21068  divcn  21102  cdivcncf  21151  bcth3  21500  ismbl2  21668  cmmbl  21675  nulmbl  21676  nulmbl2  21677  unmbl  21678  voliunlem1  21690  voliunlem2  21691  ioombl1lem4  21701  ioombl1  21702  uniioombllem3  21724  mbfss  21783  itg1cl  21822  itg1ge0  21823  i1f0  21824  i1f1  21827  i1fmul  21833  itg1addlem4  21836  itg1mulc  21841  itg10a  21847  itg1ge0a  21848  itg1climres  21851  itg2cnlem1  21898  itgioo  21952  itgsplitioo  21974  limcdif  22010  ellimc2  22011  ellimc3  22013  limcflflem  22014  limcflf  22015  limcmo  22016  limcresi  22019  dvreslem  22043  dvres2lem  22044  dvidlem  22049  dvcnp2  22053  dvaddbr  22071  dvmulbr  22072  dvcobr  22079  dvrec  22088  dvcnvlem  22107  lhop1lem  22144  lhop  22147  tdeglem4  22188  deg1n0ima  22219  aacjcl  22452  taylthlem2  22498  abelth  22565  logcnlem5  22750  dvlog2  22757  efopnlem2  22761  cxpcn2  22843  sqrcn  22847  efrlim  23022  jensen  23041  amgm  23043  wilthlem2  23066  dchrelbas2  23235  rpvmasum2  23420  dchrisum0re  23421  dchrisum0lem3  23427  dchrisum0  23428  tgisline  23716  umgrass  23984  frgrawopreg2  24716  xrge00  27324  fsumcvg4  27556  qtophaus  27625  gsumesum  27695  pwsiga  27758  sigainb  27764  sibfof  27910  sitgclg  27912  ballotlemfelz  28057  ballotlemfp1  28058  ballotth  28104  lgamgulmlem2  28200  lgamucov  28208  kur14lem6  28283  kur14lem7  28284  cvmscld  28346  fprodss  28645  fundmpss  28761  wfi  28852  frind  28888  wfrlem16  28923  relsset  29103  limitssson  29126  fnsingle  29134  funimage  29143  mblfinlem3  29619  mblfinlem4  29620  ismblfin  29621  voliunnfl  29624  cnambfre  29629  dvtan  29631  dvcncxp1  29666  dvcnsqr  29667  dvasin  29669  dvacos  29670  areacirclem4  29676  cldbnd  29710  clsun  29712  fdc  29830  divrngcl  29952  isdrngo2  29953  isdrngo3  29954  istopclsd  30225  diophin  30299  setindtr  30561  dnnumch1  30585  cntzsdrg  30747  isdomn3  30760  deg1mhm  30763  sumnnodd  31129  cncficcgt0  31184  cncfiooicclem1  31189  dirkercncflem2  31361  fourierdlem62  31426  fourierdlem66  31430  fourierdlem68  31432  fourierdlem95  31459  lindslinindimp2lem2  32010  islsati  33668  hdmap14lem2a  36544