Theorem difss 4087

Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
difss	⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Proof of Theorem difss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 4082	. 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3938	1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Syntax hints:   ∖ cdif 3899   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-ss 3919

This theorem is referenced by:  difssd  4088  difss2  4089  ssdifss  4091  0dif  4356  disj4  4410  difsnpss  4764  unidif  4898  iunxdif2  5008  difexg  5282  difelpw  5307  reldif  5784  cnvdif  6122  difxp  6144  frpoind  6323  tz7.7  6366  fresaun  6729  fresaunres2  6730  resdif  6822  fndmdif  7017  tfi  7827  peano5  7868  oelim2  8558  swoer  8703  swoord1  8704  swoord2  8705  ralxpmap  8871  boxcutc  8916  undom  9030  domunsncan  9042  sbthlem2  9053  sbthlem4  9055  sbthlem5  9056  limenpsi  9117  diffi  9136  php3  9170  frfi  9222  fofinf1o  9268  ixpfi2  9286  elfiun  9369  marypha1lem  9372  wemapso  9492  infdifsn  9605  cantnflem2  9638  frind  9701  frr1  9710  dfac8alem  9978  acnnum  10001  inffien  10012  kmlem5  10104  infdif  10157  infdif2  10158  ackbij1lem18  10185  fictb  10193  fin23lem7  10266  fin23lem11  10267  fin23lem28  10290  fin23lem30  10292  compsscnvlem  10320  isf34lem2  10323  compssiso  10324  isf34lem4  10327  fin1a2lem7  10356  axcclem  10407  zornn0g  10455  ttukey2g  10466  pinn  10829  niex  10832  ltsopi  10839  dmaddpi  10841  dmmulpi  10842  lerelxr  11238  mulnzcnf  11826  dflt2  13143  expcl2lem  14079  expclzlem  14089  hashun2  14389  fsumss  15742  fsumless  15814  cvgcmpce  15836  fprodss  15968  rpnnen2lem9  16244  isstruct2  17175  structcnvcnv  17179  strleun  17183  strle1  17184  fsets  17195  mreexexlem2d  17667  gsumpropd2lem  18703  symgfixf1  19467  f1omvdmvd  19473  mvdco  19475  f1omvdconj  19476  pmtrfb  19495  pmtrfconj  19496  symggen  19500  symggen2  19501  psgnunilem1  19523  frgpnabllem2  19904  dprdss  20061  dprd2da  20074  dmdprdsplit2lem  20077  dpjidcl  20090  ablfac1b  20102  ablfac1eu  20105  isdomn3  20751  isdrng2  20779  drngmclOLD  20787  drngid2  20788  isdrngd  20801  isdrngdOLD  20803  cntzsdrg  20838  subdrgint  20839  cnmgpid  21468  cnmsubglem  21469  xrs1mnd  21479  xrs10  21480  xrs1cmn  21481  xrge0subm  21482  xrge0cmn  21483  expghm  21514  dsmmfi  21777  islinds2  21852  lindsind2  21858  lindfrn  21860  islindf4  21877  psdmul  22218  mdetdiaglem  22645  mdetrsca2  22651  mdetrlin2  22654  mdetralt  22655  mdetunilem5  22663  mdetunilem9  22667  maducoeval2  22687  smadiadetglem1  22718  isopn2  23079  ntrval2  23098  ntrdif  23099  clsdif  23100  ntrss  23102  cmclsopn  23109  discld  23136  mretopd  23139  lpsscls  23188  restntr  23229  cmpcld  23449  2ndcsep  23506  1stccnp  23509  llycmpkgen2  23597  1stckgen  23601  txkgen  23699  qtopcld  23760  qtopcmap  23766  kqdisj  23779  isufil2  23955  ufileu  23966  filufint  23967  fixufil  23969  cfinufil  23975  ufilen  23977  fin1aufil  23979  supnfcls  24067  flimfnfcls  24075  alexsublem  24091  alexsubALTlem3  24096  cldsubg  24158  imasdsf1olem  24420  recld2  24862  sszcld  24865  xrge0gsumle  24881  divcn  24917  cdivcncf  24970  bcth3  25380  ismbl2  25576  cmmbl  25583  nulmbl  25584  nulmbl2  25585  unmbl  25586  voliunlem1  25599  voliunlem2  25600  ioombl1lem4  25610  ioombl1  25611  uniioombllem3  25634  mbfss  25695  itg1cl  25734  itg1ge0  25735  i1f0  25736  i1f1  25739  i1fmul  25745  itg1addlem4  25748  itg1mulc  25753  itg10a  25759  itg1ge0a  25760  itg1climres  25763  itg2cnlem1  25810  itgioo  25865  itgsplitioo  25887  limcdif  25925  ellimc2  25926  ellimc3  25928  limcflflem  25929  limcflf  25930  limcmo  25931  limcresi  25934  dvreslem  25958  dvres2lem  25959  dvidlem  25964  dvcnp2  25969  dvaddbr  25987  dvmulbr  25988  dvcobr  25995  dvrec  26004  dvcnvlem  26025  lhop1lem  26062  lhop  26065  tdeglem4  26107  deg1n0ima  26136  aacjcl  26378  taylthlem2  26424  abelth  26491  logcnlem5  26698  dvlog2  26705  efopnlem2  26709  dvcncxp1  26795  dvcnsqrt  26796  cxpcn2  26798  sqrtcn  26802  efrlim  27021  jensen  27040  amgm  27042  lgamgulmlem2  27081  lgamucov  27089  wilthlem2  27120  dchrelbas2  27288  rpvmasum2  27563  dchrisum0re  27564  dchrisum0lem3  27570  dchrisum0  27571  nnssn0s  28401  tgisline  28783  upgrss  29245  frgrwopreg2  30477  difxp1ss  32680  difxp2ss  32681  xrge00  33152  symgcom2  33224  pmtrcnel  33229  pmtrcnel2  33230  pmtrcnelor  33231  cycpmrn  33283  tocyccntz  33284  prmidlsubm  33606  evlextv  33799  vietalem  33836  submatres  34063  madjusmdetlem2  34085  madjusmdetlem3  34086  qtophaus  34093  fsumcvg4  34207  gsumesum  34316  pwsiga  34387  sigainb  34393  carsggect  34575  omsmeas  34580  sitgclg  34599  ballotlemfelz  34748  ballotlemfp1  34749  ballotth  34795  cxpcncf1  34849  logdivsqrle  34904  hgt750lemb  34910  fineqvnttrclse  35380  kur14lem6  35521  kur14lem7  35522  cvmscld  35583  satfvsucsuc  35675  satfrnmapom  35680  mclsppslem  35893  fundmpss  36077  relsset  36196  limitssson  36219  fnsingle  36227  funimage  36236  cldbnd  36646  clsun  36648  topdifinffinlem  37801  inunissunidif  37829  pibt2  37871  matunitlindflem1  38075  poimirlem8  38087  poimirlem26  38105  poimirlem30  38109  mblfinlem3  38118  mblfinlem4  38119  ismblfin  38120  voliunnfl  38123  cnambfre  38127  dvtan  38129  dvasin  38163  dvacos  38164  areacirclem4  38170  fdc  38204  divrngcl  38416  isdrngo2  38417  isdrngo3  38418  islsati  39578  hdmap14lem2a  42451  redvmptabs  42929  prjspreln0  43151  prjspvs  43152  prjspeclsp  43154  0prjspnrel  43169  istopclsd  43241  diophin  43313  dnnumch1  43581  deg1mhm  43737  gneispace  44670  inaex  44833  sumnnodd  46166  cncficcgt0  46422  cncfiooicclem1  46427  cxpcncf2  46433  dirkercncflem2  46638  fourierdlem62  46702  fourierdlem66  46706  fourierdlem68  46708  fourierdlem95  46735  etransclem24  46792  etransclem44  46812  gsumge0cl  46905  sge0fodjrnlem  46950  carageniuncllem1  47055  smfresal  47322  dfnbgrss  48434  dfnbgrss2  48441  lindslinindimp2lem2  49041  iscnrm3rlem2  49522  amgmlemALT  50384