Theorem difss 4091

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

Syntax hints:   ∖ cdif 3903   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-ss 3923

This theorem is referenced by:  difssd  4092  difss2  4093  ssdifss  4095  0dif  4364  disj4  4420  difsnpss  4776  unidif  4909  iunxdif2  5019  difexg  5301  difelpw  5326  reldif  5804  cnvdif  6142  difxp  6163  frpoind  6345  tz7.7  6388  fresaun  6751  fresaunres2  6752  resdif  6844  fndmdif  7039  tfi  7850  peano5  7891  oelim2  8582  swoer  8727  swoord1  8728  swoord2  8729  ralxpmap  8895  boxcutc  8940  undom  9054  domunsncan  9066  sbthlem2  9077  sbthlem4  9079  sbthlem5  9080  limenpsi  9141  diffi  9160  php3  9194  frfi  9246  fofinf1o  9290  ixpfi2  9308  elfiun  9391  marypha1lem  9394  wemapso  9514  infdifsn  9627  cantnflem2  9660  frind  9723  frr1  9732  dfac8alem  10014  acnnum  10037  inffien  10048  kmlem5  10139  infdif  10192  infdif2  10193  ackbij1lem18  10220  fictb  10228  fin23lem7  10301  fin23lem11  10302  fin23lem28  10325  fin23lem30  10327  compsscnvlem  10355  isf34lem2  10358  compssiso  10359  isf34lem4  10362  fin1a2lem7  10391  axcclem  10442  zornn0g  10490  ttukey2g  10501  pinn  10864  niex  10867  ltsopi  10874  dmaddpi  10876  dmmulpi  10877  lerelxr  11273  mulnzcnf  11861  dflt2  13174  expcl2lem  14111  expclzlem  14121  hashun2  14421  fsumss  15778  fsumless  15850  cvgcmpce  15872  fprodss  16004  rpnnen2lem9  16279  isstruct2  17210  structcnvcnv  17214  strleun  17218  strle1  17219  fsets  17230  mreexexlem2d  17702  gsumpropd2lem  18738  symgfixf1  19508  f1omvdmvd  19514  mvdco  19516  f1omvdconj  19517  pmtrfb  19536  pmtrfconj  19537  symggen  19541  symggen2  19542  psgnunilem1  19564  frgpnabllem2  19945  dprdss  20102  dprd2da  20115  dmdprdsplit2lem  20118  dpjidcl  20131  ablfac1b  20143  ablfac1eu  20146  isdomn3  20800  isdrng2  20830  drngid2  20838  isdrngd  20850  isdrngdOLD  20852  cntzsdrg  20886  subdrgint  20887  prmidlsubm  21468  cnmgpid  21560  cnmsubglem  21561  xrs1mnd  21571  xrs10  21572  xrs1cmn  21573  xrge0subm  21574  xrge0cmn  21575  expghm  21606  dsmmfi  21869  islinds2  21944  lindsind2  21950  lindfrn  21952  islindf4  21969  psdmul  22310  mdetdiaglem  22736  mdetrsca2  22742  mdetrlin2  22745  mdetralt  22746  mdetunilem5  22754  mdetunilem9  22758  maducoeval2  22778  smadiadetglem1  22809  isopn2  23170  ntrval2  23189  ntrdif  23190  clsdif  23191  ntrss  23193  cmclsopn  23200  discld  23227  mretopd  23230  lpsscls  23279  restntr  23320  cmpcld  23540  2ndcsep  23597  1stccnp  23600  llycmpkgen2  23688  1stckgen  23692  txkgen  23790  qtopcld  23851  qtopcmap  23857  kqdisj  23870  isufil2  24046  ufileu  24057  filufint  24058  fixufil  24060  cfinufil  24066  ufilen  24068  fin1aufil  24070  supnfcls  24158  flimfnfcls  24166  alexsublem  24182  alexsubALTlem3  24187  cldsubg  24249  imasdsf1olem  24511  recld2  24953  sszcld  24956  xrge0gsumle  24972  divcn  25008  cdivcncf  25061  bcth3  25471  ismbl2  25667  cmmbl  25674  nulmbl  25675  nulmbl2  25676  unmbl  25677  voliunlem1  25690  voliunlem2  25691  ioombl1lem4  25701  ioombl1  25702  uniioombllem3  25725  mbfss  25786  itg1cl  25825  itg1ge0  25826  i1f0  25827  i1f1  25830  i1fmul  25836  itg1addlem4  25839  itg1mulc  25844  itg10a  25850  itg1ge0a  25851  itg1climres  25854  itg2cnlem1  25901  itgioo  25956  itgsplitioo  25978  limcdif  26016  ellimc2  26017  ellimc3  26019  limcflflem  26020  limcflf  26021  limcmo  26022  limcresi  26025  dvreslem  26049  dvres2lem  26050  dvidlem  26055  dvcnp2  26060  dvaddbr  26078  dvmulbr  26079  dvcobr  26086  dvrec  26095  dvcnvlem  26116  lhop1lem  26153  lhop  26156  tdeglem4  26198  deg1n0ima  26227  aacjcl  26471  taylthlem2  26518  abelth  26585  logcnlem5  26792  dvlog2  26799  efopnlem2  26803  dvcncxp1  26889  dvcnsqrt  26890  cxpcn2  26892  sqrtcn  26896  efrlim  27115  jensen  27134  amgm  27136  lgamgulmlem2  27175  lgamucov  27183  wilthlem2  27214  dchrelbas2  27382  rpvmasum2  27657  dchrisum0re  27658  dchrisum0lem3  27664  dchrisum0  27665  nnssn0s  28495  tgisline  28881  upgrss  29419  frgrwopreg2  30651  difxp1ss  32849  difxp2ss  32850  xrge00  33315  symgcom2  33385  pmtrcnel  33390  pmtrcnel2  33391  pmtrcnelor  33392  cycpmrn  33444  tocyccntz  33445  evlextv  33913  vietalem  33950  submatres  34177  madjusmdetlem2  34199  madjusmdetlem3  34200  qtophaus  34207  fsumcvg4  34321  gsumesum  34430  pwsiga  34501  sigainb  34507  carsggect  34689  omsmeas  34694  sitgclg  34713  ballotlemfelz  34862  ballotlemfp1  34863  ballotth  34909  cxpcncf1  34963  logdivsqrle  35018  hgt750lemb  35024  fineqvnttrclse  35518  kur14lem6  35684  kur14lem7  35685  cvmscld  35746  satfvsucsuc  35838  satfrnmapom  35843  mclsppslem  36056  fundmpss  36240  relsset  36359  limitssson  36382  fnsingle  36390  funimage  36399  cldbnd  36818  clsun  36820  topdifinffinlem  37974  inunissunidif  38002  pibt2  38044  matunitlindflem1  38248  poimirlem8  38260  poimirlem26  38278  poimirlem30  38282  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  voliunnfl  38296  cnambfre  38300  dvtan  38302  dvasin  38336  dvacos  38337  areacirclem4  38343  fdc  38377  divrngcl  38589  isdrngo2  38590  isdrngo3  38591  islsati  39749  hdmap14lem2a  42622  redvmptabs  43102  prjspreln0  43324  prjspvs  43325  prjspeclsp  43327  0prjspnrel  43342  istopclsd  43414  diophin  43486  dnnumch1  43754  deg1mhm  43910  gneispace  44843  inaex  44990  sumnnodd  46329  cncficcgt0  46585  cncfiooicclem1  46590  cxpcncf2  46596  dirkercncflem2  46801  fourierdlem62  46865  fourierdlem66  46869  fourierdlem68  46871  fourierdlem95  46898  etransclem24  46955  etransclem44  46975  gsumge0cl  47068  sge0fodjrnlem  47113  carageniuncllem1  47218  smfresal  47485  dfnbgrss  48600  dfnbgrss2  48607  lindslinindimp2lem2  49222  iscnrm3rlem2  49702  amgmlemALT  50586