Theorem difss 4077

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 4072	. 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3926	1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Syntax hints:   ∖ cdif 3887   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907

This theorem is referenced by:  difssd  4078  difss2  4079  ssdifss  4081  0dif  4346  disj4  4400  difsnpss  4751  unidif  4886  iunxdif2  4997  difexg  5266  difelpw  5291  reldif  5764  cnvdif  6101  difxp  6122  frpoind  6300  tz7.7  6343  fresaun  6705  fresaunres2  6706  resdif  6795  fndmdif  6988  tfi  7797  peano5  7837  oelim2  8524  swoer  8668  swoord1  8669  swoord2  8670  ralxpmap  8837  boxcutc  8882  undom  8996  domunsncan  9008  sbthlem2  9019  sbthlem4  9021  sbthlem5  9022  limenpsi  9083  diffi  9102  php3  9136  frfi  9188  fofinf1o  9235  ixpfi2  9253  elfiun  9336  marypha1lem  9339  wemapso  9459  infdifsn  9569  cantnflem2  9602  frind  9665  frr1  9674  dfac8alem  9942  acnnum  9965  inffien  9976  kmlem5  10068  infdif  10121  infdif2  10122  ackbij1lem18  10149  fictb  10157  fin23lem7  10229  fin23lem11  10230  fin23lem28  10253  fin23lem30  10255  compsscnvlem  10283  isf34lem2  10286  compssiso  10287  isf34lem4  10290  fin1a2lem7  10319  axcclem  10370  zornn0g  10418  ttukey2g  10429  pinn  10792  niex  10795  ltsopi  10802  dmaddpi  10804  dmmulpi  10805  lerelxr  11199  mulnzcnf  11787  dflt2  13090  expcl2lem  14026  expclzlem  14036  hashun2  14336  fsumss  15678  fsumless  15750  cvgcmpce  15772  fprodss  15904  rpnnen2lem9  16180  isstruct2  17110  structcnvcnv  17114  strleun  17118  strle1  17119  fsets  17130  mreexexlem2d  17602  gsumpropd2lem  18638  symgfixf1  19403  f1omvdmvd  19409  mvdco  19411  f1omvdconj  19412  pmtrfb  19431  pmtrfconj  19432  symggen  19436  symggen2  19437  psgnunilem1  19459  frgpnabllem2  19840  dprdss  19997  dprd2da  20010  dmdprdsplit2lem  20013  dpjidcl  20026  ablfac1b  20038  ablfac1eu  20041  isdomn3  20683  isdrng2  20711  drngmclOLD  20719  drngid2  20720  isdrngd  20733  isdrngdOLD  20735  cntzsdrg  20770  subdrgint  20771  cnmgpid  21419  cnmsubglem  21420  xrs1mnd  21430  xrs10  21431  xrs1cmn  21432  xrge0subm  21433  xrge0cmn  21434  expghm  21465  dsmmfi  21728  islinds2  21803  lindsind2  21809  lindfrn  21811  islindf4  21828  psdmul  22142  mdetdiaglem  22573  mdetrsca2  22579  mdetrlin2  22582  mdetralt  22583  mdetunilem5  22591  mdetunilem9  22595  maducoeval2  22615  smadiadetglem1  22646  isopn2  23007  ntrval2  23026  ntrdif  23027  clsdif  23028  ntrss  23030  cmclsopn  23037  discld  23064  mretopd  23067  lpsscls  23116  restntr  23157  cmpcld  23377  2ndcsep  23434  1stccnp  23437  llycmpkgen2  23525  1stckgen  23529  txkgen  23627  qtopcld  23688  qtopcmap  23694  kqdisj  23707  isufil2  23883  ufileu  23894  filufint  23895  fixufil  23897  cfinufil  23903  ufilen  23905  fin1aufil  23907  supnfcls  23995  flimfnfcls  24003  alexsublem  24019  alexsubALTlem3  24024  cldsubg  24086  imasdsf1olem  24348  recld2  24790  sszcld  24793  xrge0gsumle  24809  divcn  24845  cdivcncf  24898  bcth3  25308  ismbl2  25504  cmmbl  25511  nulmbl  25512  nulmbl2  25513  unmbl  25514  voliunlem1  25527  voliunlem2  25528  ioombl1lem4  25538  ioombl1  25539  uniioombllem3  25562  mbfss  25623  itg1cl  25662  itg1ge0  25663  i1f0  25664  i1f1  25667  i1fmul  25673  itg1addlem4  25676  itg1mulc  25681  itg10a  25687  itg1ge0a  25688  itg1climres  25691  itg2cnlem1  25738  itgioo  25793  itgsplitioo  25815  limcdif  25853  ellimc2  25854  ellimc3  25856  limcflflem  25857  limcflf  25858  limcmo  25859  limcresi  25862  dvreslem  25886  dvres2lem  25887  dvidlem  25892  dvcnp2  25897  dvaddbr  25915  dvmulbr  25916  dvcobr  25923  dvrec  25932  dvcnvlem  25953  lhop1lem  25990  lhop  25993  tdeglem4  26035  deg1n0ima  26064  aacjcl  26304  taylthlem2  26351  taylthlem2OLD  26352  abelth  26419  logcnlem5  26623  dvlog2  26630  efopnlem2  26634  dvcncxp1  26720  dvcnsqrt  26721  cxpcn2  26723  sqrtcn  26727  efrlim  26946  efrlimOLD  26947  jensen  26966  amgm  26968  lgamgulmlem2  27007  lgamucov  27015  wilthlem2  27046  dchrelbas2  27214  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem3  27496  dchrisum0  27497  nnssn0s  28327  tgisline  28709  upgrss  29171  frgrwopreg2  30404  difxp1ss  32607  difxp2ss  32608  xrge00  33089  symgcom2  33160  pmtrcnel  33165  pmtrcnel2  33166  pmtrcnelor  33167  cycpmrn  33219  tocyccntz  33220  evlextv  33701  vietalem  33738  submatres  33966  madjusmdetlem2  33988  madjusmdetlem3  33989  qtophaus  33996  fsumcvg4  34110  gsumesum  34219  pwsiga  34290  sigainb  34296  carsggect  34478  omsmeas  34483  sitgclg  34502  ballotlemfelz  34651  ballotlemfp1  34652  ballotth  34698  cxpcncf1  34755  logdivsqrle  34810  hgt750lemb  34816  fineqvnttrclse  35284  kur14lem6  35409  kur14lem7  35410  cvmscld  35471  satfvsucsuc  35563  satfrnmapom  35568  mclsppslem  35781  fundmpss  35965  relsset  36084  limitssson  36107  fnsingle  36115  funimage  36124  cldbnd  36524  clsun  36526  topdifinffinlem  37677  inunissunidif  37705  pibt2  37747  matunitlindflem1  37951  poimirlem8  37963  poimirlem26  37981  poimirlem30  37985  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  voliunnfl  37999  cnambfre  38003  dvtan  38005  dvasin  38039  dvacos  38040  areacirclem4  38046  fdc  38080  divrngcl  38292  isdrngo2  38293  isdrngo3  38294  islsati  39454  hdmap14lem2a  42327  redvmptabs  42806  prjspreln0  43056  prjspvs  43057  prjspeclsp  43059  0prjspnrel  43074  istopclsd  43146  diophin  43218  dnnumch1  43490  deg1mhm  43646  gneispace  44579  inaex  44742  sumnnodd  46078  cncficcgt0  46334  cncfiooicclem1  46339  cxpcncf2  46345  dirkercncflem2  46550  fourierdlem62  46614  fourierdlem66  46618  fourierdlem68  46620  fourierdlem95  46647  etransclem24  46704  etransclem44  46724  gsumge0cl  46817  sge0fodjrnlem  46862  carageniuncllem1  46967  smfresal  47234  dfnbgrss  48340  dfnbgrss2  48347  lindslinindimp2lem2  48947  iscnrm3rlem2  49428  amgmlemALT  50290