Theorem difss 3737

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

Syntax hints:   \ cdif 3571   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  difssd  3738  difss2  3739  ssdifss  3741  0dif  3977  disj4  4025  uneqdifeqOLD  4058  difsnpss  4338  unidif  4471  iunxdif2  4568  difexg  4808  reldif  5238  cnvdif  5539  difxp  5558  wfi  5713  tz7.7  5749  fresaun  6075  fresaunres2  6076  resdif  6157  fndmdif  6321  tfi  7053  peano5  7089  wfrlem16  7430  oev  7594  oelim2  7675  swoer  7772  swoord1  7773  swoord2  7774  ralxpmap  7907  boxcutc  7951  undom  8048  domunsncan  8060  sbthlem2  8071  sbthlem4  8073  sbthlem5  8074  limenpsi  8135  phplem2  8140  php  8144  php3  8146  pssnn  8178  diffi  8192  frfi  8205  fofinf1o  8241  ixpfi2  8264  elfiun  8336  marypha1lem  8339  wemapso  8456  infdifsn  8554  cantnflem2  8587  dfac8alem  8852  acnnum  8875  inffien  8886  kmlem5  8976  infdif  9031  infdif2  9032  ackbij1lem18  9059  fictb  9067  fin23lem7  9138  fin23lem11  9139  fin23lem28  9162  fin23lem30  9164  compsscnvlem  9192  isf34lem2  9195  compssiso  9196  isf34lem4  9199  fin1a2lem7  9228  domtriomlem  9264  axcclem  9279  zornn0g  9327  ttukey2g  9338  konigthlem  9390  pinn  9700  niex  9703  ltsopi  9710  dmaddpi  9712  dmmulpi  9713  lerelxr  10101  mulnzcnopr  10673  dflt2  11981  expcl2lem  12872  expclzlem  12884  hashun2  13172  fsumss  14456  fsumless  14528  cvgcmpce  14550  fprodss  14678  rpnnen2lem9  14951  isstruct2  15867  structcnvcnv  15871  fsets  15891  strleun  15972  strle1  15973  mreexexlem2d  16305  gsumpropd2lem  17273  symgfixf1  17857  f1omvdmvd  17863  mvdco  17865  f1omvdconj  17866  pmtrfb  17885  pmtrfconj  17886  symggen  17890  symggen2  17891  psgnunilem1  17913  frgpnabllem2  18277  dprdss  18428  dprd2da  18441  dmdprdsplit2lem  18444  dpjidcl  18457  ablfac1b  18469  ablfac1eu  18472  isdrng2  18757  drngmcl  18760  drngid2  18763  isdrngd  18772  xrs1mnd  19784  xrs10  19785  xrs1cmn  19786  xrge0subm  19787  xrge0cmn  19788  cnmgpid  19808  cnmsubglem  19809  expghm  19844  cnmsgngrp  19925  psgninv  19928  dsmmfi  20082  islinds2  20152  lindsind2  20158  lindfrn  20160  islindf4  20177  mdetdiaglem  20404  mdetrsca2  20410  mdetrlin2  20413  mdetralt  20414  mdetunilem5  20422  mdetunilem9  20426  maducoeval2  20446  smadiadetglem1  20477  isopn2  20836  ntrval2  20855  ntrdif  20856  clsdif  20857  ntrss  20859  cmclsopn  20866  discld  20893  mretopd  20896  lpsscls  20945  restntr  20986  cmpcld  21205  2ndcsep  21262  1stccnp  21265  llycmpkgen2  21353  1stckgen  21357  txkgen  21455  qtopcld  21516  qtopcmap  21522  kqdisj  21535  isufil2  21712  ufileu  21723  filufint  21724  fixufil  21726  cfinufil  21732  ufilen  21734  fin1aufil  21736  supnfcls  21824  flimfnfcls  21832  alexsublem  21848  alexsubALTlem3  21853  cldsubg  21914  imasdsf1olem  22178  recld2  22617  sszcld  22620  xrge0gsumle  22636  divcn  22671  cdivcncf  22720  bcth3  23128  ismbl2  23295  cmmbl  23302  nulmbl  23303  nulmbl2  23304  unmbl  23305  voliunlem1  23318  voliunlem2  23319  ioombl1lem4  23329  ioombl1  23330  uniioombllem3  23353  mbfss  23413  itg1cl  23452  itg1ge0  23453  i1f0  23454  i1f1  23457  i1fmul  23463  itg1addlem4  23466  itg1mulc  23471  itg10a  23477  itg1ge0a  23478  itg1climres  23481  itg2cnlem1  23528  itgioo  23582  itgsplitioo  23604  limcdif  23640  ellimc2  23641  ellimc3  23643  limcflflem  23644  limcflf  23645  limcmo  23646  limcresi  23649  dvreslem  23673  dvres2lem  23674  dvidlem  23679  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvrec  23718  dvcnvlem  23739  lhop1lem  23776  lhop  23779  tdeglem4  23820  deg1n0ima  23849  aacjcl  24082  taylthlem2  24128  abelth  24195  logcnlem5  24392  dvlog2  24399  efopnlem2  24403  dvcncxp1  24484  dvcnsqrt  24485  cxpcn2  24487  sqrtcn  24491  efrlim  24696  jensen  24715  amgm  24717  lgamgulmlem2  24756  lgamucov  24764  wilthlem2  24795  dchrelbas2  24962  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem3  25208  dchrisum0  25209  tgisline  25522  upgrss  25983  frgrwopreg2  27183  xrge00  29686  submatres  29872  madjusmdetlem2  29894  madjusmdetlem3  29895  qtophaus  29903  fsumcvg4  29996  gsumesum  30121  pwsiga  30193  sigainb  30199  carsggect  30380  omsmeas  30385  sitgclg  30404  ballotlemfelz  30552  ballotlemfp1  30553  ballotth  30599  cxpcncf1  30673  logdivsqrle  30728  hgt750lemb  30734  kur14lem6  31193  kur14lem7  31194  cvmscld  31255  mclsppslem  31480  fundmpss  31664  frind  31740  relsset  31995  limitssson  32018  fnsingle  32026  funimage  32035  cldbnd  32321  clsun  32323  topdifinffinlem  33195  matunitlindflem1  33405  poimirlem8  33417  poimirlem26  33435  poimirlem30  33439  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  voliunnfl  33453  cnambfre  33458  dvtan  33460  dvasin  33496  dvacos  33497  areacirclem4  33503  fdc  33541  divrngcl  33756  isdrngo2  33757  isdrngo3  33758  islsati  34281  hdmap14lem2a  37159  istopclsd  37263  diophin  37336  dnnumch1  37614  cntzsdrg  37772  isdomn3  37782  deg1mhm  37785  gneispace  38432  sumnnodd  39862  cncficcgt0  40101  cncfiooicclem1  40106  cxpcncf2  40113  dirkercncflem2  40321  fourierdlem62  40385  fourierdlem66  40389  fourierdlem68  40391  fourierdlem95  40418  etransclem24  40475  etransclem44  40495  gsumge0cl  40588  sge0fodjrnlem  40633  carageniuncllem1  40735  smfresal  40995  lindslinindimp2lem2  42248  amgmlemALT  42549