Theorem difss 4088

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

Syntax hints:   ∖ cdif 3898   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918

This theorem is referenced by:  difssd  4089  difss2  4090  ssdifss  4092  0dif  4357  disj4  4411  difsnpss  4763  unidif  4898  iunxdif2  5009  difexg  5274  difelpw  5299  reldif  5764  cnvdif  6101  difxp  6122  frpoind  6300  tz7.7  6343  fresaun  6705  fresaunres2  6706  resdif  6795  fndmdif  6987  tfi  7795  peano5  7835  oelim2  8523  swoer  8666  swoord1  8667  swoord2  8668  ralxpmap  8834  boxcutc  8879  undom  8993  domunsncan  9005  sbthlem2  9016  sbthlem4  9018  sbthlem5  9019  limenpsi  9080  diffi  9099  php3  9133  frfi  9185  fofinf1o  9232  ixpfi2  9250  elfiun  9333  marypha1lem  9336  wemapso  9456  infdifsn  9566  cantnflem2  9599  frind  9662  frr1  9671  dfac8alem  9939  acnnum  9962  inffien  9973  kmlem5  10065  infdif  10118  infdif2  10119  ackbij1lem18  10146  fictb  10154  fin23lem7  10226  fin23lem11  10227  fin23lem28  10250  fin23lem30  10252  compsscnvlem  10280  isf34lem2  10283  compssiso  10284  isf34lem4  10287  fin1a2lem7  10316  axcclem  10367  zornn0g  10415  ttukey2g  10426  pinn  10789  niex  10792  ltsopi  10799  dmaddpi  10801  dmmulpi  10802  lerelxr  11195  mulnzcnf  11783  dflt2  13062  expcl2lem  13996  expclzlem  14006  hashun2  14306  fsumss  15648  fsumless  15719  cvgcmpce  15741  fprodss  15871  rpnnen2lem9  16147  isstruct2  17076  structcnvcnv  17080  strleun  17084  strle1  17085  fsets  17096  mreexexlem2d  17568  gsumpropd2lem  18604  symgfixf1  19366  f1omvdmvd  19372  mvdco  19374  f1omvdconj  19375  pmtrfb  19394  pmtrfconj  19395  symggen  19399  symggen2  19400  psgnunilem1  19422  frgpnabllem2  19803  dprdss  19960  dprd2da  19973  dmdprdsplit2lem  19976  dpjidcl  19989  ablfac1b  20001  ablfac1eu  20004  isdomn3  20648  isdrng2  20676  drngmclOLD  20684  drngid2  20685  isdrngd  20698  isdrngdOLD  20700  cntzsdrg  20735  subdrgint  20736  cnmgpid  21384  cnmsubglem  21385  xrs1mnd  21395  xrs10  21396  xrs1cmn  21397  xrge0subm  21398  xrge0cmn  21399  expghm  21430  dsmmfi  21693  islinds2  21768  lindsind2  21774  lindfrn  21776  islindf4  21793  psdmul  22109  mdetdiaglem  22542  mdetrsca2  22548  mdetrlin2  22551  mdetralt  22552  mdetunilem5  22560  mdetunilem9  22564  maducoeval2  22584  smadiadetglem1  22615  isopn2  22976  ntrval2  22995  ntrdif  22996  clsdif  22997  ntrss  22999  cmclsopn  23006  discld  23033  mretopd  23036  lpsscls  23085  restntr  23126  cmpcld  23346  2ndcsep  23403  1stccnp  23406  llycmpkgen2  23494  1stckgen  23498  txkgen  23596  qtopcld  23657  qtopcmap  23663  kqdisj  23676  isufil2  23852  ufileu  23863  filufint  23864  fixufil  23866  cfinufil  23872  ufilen  23874  fin1aufil  23876  supnfcls  23964  flimfnfcls  23972  alexsublem  23988  alexsubALTlem3  23993  cldsubg  24055  imasdsf1olem  24317  recld2  24759  sszcld  24762  xrge0gsumle  24778  divcnOLD  24813  divcn  24815  cdivcncf  24870  bcth3  25287  ismbl2  25484  cmmbl  25491  nulmbl  25492  nulmbl2  25493  unmbl  25494  voliunlem1  25507  voliunlem2  25508  ioombl1lem4  25518  ioombl1  25519  uniioombllem3  25542  mbfss  25603  itg1cl  25642  itg1ge0  25643  i1f0  25644  i1f1  25647  i1fmul  25653  itg1addlem4  25656  itg1mulc  25661  itg10a  25667  itg1ge0a  25668  itg1climres  25671  itg2cnlem1  25718  itgioo  25773  itgsplitioo  25795  limcdif  25833  ellimc2  25834  ellimc3  25836  limcflflem  25837  limcflf  25838  limcmo  25839  limcresi  25842  dvreslem  25866  dvres2lem  25867  dvidlem  25872  dvcnp2  25877  dvcnp2OLD  25878  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcobr  25905  dvcobrOLD  25906  dvrec  25915  dvcnvlem  25936  lhop1lem  25974  lhop  25977  tdeglem4  26021  deg1n0ima  26050  aacjcl  26291  taylthlem2  26338  taylthlem2OLD  26339  abelth  26407  logcnlem5  26611  dvlog2  26618  efopnlem2  26622  dvcncxp1  26708  dvcnsqrt  26709  cxpcn2  26712  sqrtcn  26716  efrlim  26935  efrlimOLD  26936  jensen  26955  amgm  26957  lgamgulmlem2  26996  lgamucov  27004  wilthlem2  27035  dchrelbas2  27204  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem3  27486  dchrisum0  27487  nnssn0s  28317  tgisline  28699  upgrss  29161  frgrwopreg2  30394  difxp1ss  32597  difxp2ss  32598  xrge00  33096  symgcom2  33166  pmtrcnel  33171  pmtrcnel2  33172  pmtrcnelor  33173  cycpmrn  33225  tocyccntz  33226  evlextv  33707  vietalem  33735  submatres  33963  madjusmdetlem2  33985  madjusmdetlem3  33986  qtophaus  33993  fsumcvg4  34107  gsumesum  34216  pwsiga  34287  sigainb  34293  carsggect  34475  omsmeas  34480  sitgclg  34499  ballotlemfelz  34648  ballotlemfp1  34649  ballotth  34695  cxpcncf1  34752  logdivsqrle  34807  hgt750lemb  34813  fineqvnttrclse  35280  kur14lem6  35405  kur14lem7  35406  cvmscld  35467  satfvsucsuc  35559  satfrnmapom  35564  mclsppslem  35777  fundmpss  35961  relsset  36080  limitssson  36103  fnsingle  36111  funimage  36120  cldbnd  36520  clsun  36522  topdifinffinlem  37552  inunissunidif  37580  pibt2  37622  matunitlindflem1  37817  poimirlem8  37829  poimirlem26  37847  poimirlem30  37851  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  voliunnfl  37865  cnambfre  37869  dvtan  37871  dvasin  37905  dvacos  37906  areacirclem4  37912  fdc  37946  divrngcl  38158  isdrngo2  38159  isdrngo3  38160  islsati  39254  hdmap14lem2a  42127  redvmptabs  42615  prjspreln0  42852  prjspvs  42853  prjspeclsp  42855  0prjspnrel  42870  istopclsd  42942  diophin  43014  dnnumch1  43286  deg1mhm  43442  gneispace  44375  inaex  44538  sumnnodd  45876  cncficcgt0  46132  cncfiooicclem1  46137  cxpcncf2  46143  dirkercncflem2  46348  fourierdlem62  46412  fourierdlem66  46416  fourierdlem68  46418  fourierdlem95  46445  etransclem24  46502  etransclem44  46522  gsumge0cl  46615  sge0fodjrnlem  46660  carageniuncllem1  46765  smfresal  47032  dfnbgrss  48098  dfnbgrss2  48105  lindslinindimp2lem2  48705  iscnrm3rlem2  49186  amgmlemALT  50048