Theorem difss 3616

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

Syntax hints:   \ cdif 3458   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475

This theorem is referenced by:  difssd  3617  difss2  3618  ssdifss  3620  disj4  3861  0dif  3885  uneqdifeq  3902  difsnpss  4158  unidif  4268  iunxdif2  4363  difexg  4585  tz7.7  4894  reldif  5112  cnvdif  5402  difxp  5421  fresaun  5746  fresaunres2  5747  resdif  5826  fndmdif  5976  tfi  6673  peano5  6708  oev  7166  oelim2  7246  swoer  7341  swoord1  7342  swoord2  7343  ralxpmap  7470  boxcutc  7514  undom  7607  domunsncan  7619  sbthlem2  7630  sbthlem4  7632  sbthlem5  7633  limenpsi  7694  phplem2  7699  php  7703  php3  7705  pssnn  7740  diffi  7753  frfi  7767  fofinf1o  7803  ixpfi2  7820  elfiun  7892  marypha1lem  7895  wemapso  7979  inf3lem3  8050  infdifsn  8076  cantnflem2  8112  dfac8alem  8413  acnnum  8436  inffien  8447  kmlem5  8537  infdif  8592  infdif2  8593  ackbij1lem18  8620  fictb  8628  fin23lem7  8699  fin23lem11  8700  fin23lem28  8723  fin23lem30  8725  compsscnvlem  8753  isf34lem2  8756  compssiso  8757  isf34lem4  8760  fin1a2lem7  8789  domtriomlem  8825  axcclem  8840  zornn0g  8888  ttukey2g  8899  konigthlem  8946  pinn  9259  niex  9262  ltsopi  9269  dmaddpi  9271  dmmulpi  9272  lerelxr  9653  mulnzcnopr  10202  dflt2  11365  expcl2lem  12160  expclzlem  12172  hashun2  12433  fsumss  13529  fsumless  13592  cvgcmpce  13614  fprodss  13737  rpnnen2lem9  13938  isstruct2  14623  structcnvcnv  14625  fsets  14640  strleun  14709  strle1  14710  mreexexlem2d  15024  gsumpropd2lem  15879  symgfixf1  16441  f1omvdmvd  16447  mvdco  16449  f1omvdconj  16450  pmtrfb  16469  pmtrfconj  16470  symggen  16474  symggen2  16475  psgnunilem1  16497  frgpnabllem2  16857  dprdss  17055  dprd2da  17070  dmdprdsplit2lem  17073  dpjidcl  17086  dpjidclOLD  17093  ablfac1b  17100  ablfac1eu  17103  isdrng2  17385  drngmcl  17388  drngid2  17391  isdrngd  17400  xrs1mnd  18435  xrs10  18436  xrs1cmn  18437  xrge0subm  18438  xrge0cmn  18439  cnmsubglem  18459  expghm  18507  expghmOLD  18508  cnmsgngrp  18593  psgninv  18596  dsmmfi  18747  islinds2  18826  lindsind2  18832  lindfrn  18834  islindf4  18851  mdetdiaglem  19078  mdetrsca2  19084  mdetrlin2  19087  mdetralt  19088  mdetunilem5  19096  mdetunilem9  19100  maducoeval2  19120  smadiadetglem1  19151  isopn2  19511  ntrval2  19530  ntrdif  19531  clsdif  19532  ntrss  19534  cmclsopn  19541  cmntrcld  19542  discld  19568  mretopd  19571  lpsscls  19620  restntr  19661  cmpcld  19880  2ndcsep  19938  1stccnp  19941  llycmpkgen2  20029  1stckgen  20033  txkgen  20131  qtopcld  20192  qtopcmap  20198  kqdisj  20211  isufil2  20387  ufileu  20398  filufint  20399  fixufil  20401  cfinufil  20407  ufilen  20409  fin1aufil  20411  supnfcls  20499  flimfnfcls  20507  alexsublem  20522  alexsubALTlem3  20527  cldsubg  20587  imasdsf1olem  20854  recld2  21297  sszcld  21300  xrge0gsumle  21316  divcn  21350  cdivcncf  21399  bcth3  21748  ismbl2  21916  cmmbl  21923  nulmbl  21924  nulmbl2  21925  unmbl  21926  voliunlem1  21938  voliunlem2  21939  ioombl1lem4  21949  ioombl1  21950  uniioombllem3  21972  mbfss  22031  itg1cl  22070  itg1ge0  22071  i1f0  22072  i1f1  22075  i1fmul  22081  itg1addlem4  22084  itg1mulc  22089  itg10a  22095  itg1ge0a  22096  itg1climres  22099  itg2cnlem1  22146  itgioo  22200  itgsplitioo  22222  limcdif  22258  ellimc2  22259  ellimc3  22261  limcflflem  22262  limcflf  22263  limcmo  22264  limcresi  22267  dvreslem  22291  dvres2lem  22292  dvidlem  22297  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvcobr  22327  dvrec  22336  dvcnvlem  22355  lhop1lem  22392  lhop  22395  tdeglem4  22436  deg1n0ima  22467  aacjcl  22701  taylthlem2  22747  abelth  22814  logcnlem5  23005  dvlog2  23012  efopnlem2  23016  cxpcn2  23098  sqrtcn  23102  efrlim  23277  jensen  23296  amgm  23298  wilthlem2  23321  dchrelbas2  23490  rpvmasum2  23675  dchrisum0re  23676  dchrisum0lem3  23682  dchrisum0  23683  tgisline  23985  umgrass  24297  frgrawopreg2  25029  xrge00  27652  qtophaus  27817  fsumcvg4  27910  gsumesum  28045  pwsiga  28108  sigainb  28114  sitgclg  28262  ballotlemfelz  28407  ballotlemfp1  28408  ballotth  28454  lgamgulmlem2  28550  lgamucov  28558  kur14lem6  28633  kur14lem7  28634  cvmscld  28696  mclsppslem  28921  fundmpss  29172  wfi  29263  frind  29299  wfrlem16  29334  relsset  29514  limitssson  29537  fnsingle  29545  funimage  29554  mblfinlem3  30029  mblfinlem4  30030  ismblfin  30031  voliunnfl  30034  cnambfre  30039  dvtan  30041  dvcncxp1  30076  dvcnsqrt  30077  dvasin  30079  dvacos  30080  areacirclem4  30086  cldbnd  30120  clsun  30122  fdc  30214  divrngcl  30336  isdrngo2  30337  isdrngo3  30338  istopclsd  30608  diophin  30682  setindtr  30942  dnnumch1  30966  cntzsdrg  31127  isdomn3  31140  deg1mhm  31143  sumnnodd  31590  cncficcgt0  31645  cncfiooicclem1  31650  cxpcncf2  31657  dirkercncflem2  31840  fourierdlem62  31905  fourierdlem66  31909  fourierdlem68  31911  fourierdlem95  31938  etransclem24  31995  etransclem44  32015  lindslinindimp2lem2  32930  islsati  34594  hdmap14lem2a  37472