Theorem difss 3947

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

Syntax hints:   ∖ cdif 3777   ⊆ wss 3780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-dif 3783  df-in 3787  df-ss 3794

This theorem is referenced by:  difssd  3948  difss2  3949  ssdifss  3951  0dif  4186  disj4  4234  difsnpss  4539  unidif  4676  iunxdif2  4771  difexg  5016  reldif  5454  cnvdif  5764  difxp  5783  wfi  5940  tz7.7  5976  fresaun  6300  fresaunres2  6301  resdif  6383  fndmdif  6553  tfi  7293  peano5  7329  wfrlem16  7676  oev  7841  oelim2  7922  swoer  8019  swoord1  8020  swoord2  8021  ralxpmap  8154  boxcutc  8198  undom  8297  domunsncan  8309  sbthlem2  8320  sbthlem4  8322  sbthlem5  8323  limenpsi  8384  phplem2  8389  php  8393  php3  8395  pssnn  8427  diffi  8441  frfi  8454  fofinf1o  8490  ixpfi2  8513  elfiun  8585  marypha1lem  8588  wemapso  8705  infdifsn  8811  cantnflem2  8844  dfac8alem  9145  acnnum  9168  inffien  9179  kmlem5  9271  infdif  9326  infdif2  9327  ackbij1lem18  9354  fictb  9362  fin23lem7  9433  fin23lem11  9434  fin23lem28  9457  fin23lem30  9459  compsscnvlem  9487  isf34lem2  9490  compssiso  9491  isf34lem4  9494  fin1a2lem7  9523  domtriomlem  9559  axcclem  9574  zornn0g  9622  ttukey2g  9633  konigthlem  9685  pinn  9995  niex  9998  ltsopi  10005  dmaddpi  10007  dmmulpi  10008  lerelxr  10396  mulnzcnopr  10968  dflt2  12217  expcl2lem  13115  expclzlem  13127  hashun2  13410  fsumss  14699  fsumless  14770  cvgcmpce  14792  fprodss  14919  rpnnen2lem9  15191  isstruct2  16098  structcnvcnv  16102  fsets  16122  strleun  16203  strle1  16204  mreexexlem2d  16530  gsumpropd2lem  17498  symgfixf1  18078  f1omvdmvd  18084  mvdco  18086  f1omvdconj  18087  pmtrfb  18106  pmtrfconj  18107  symggen  18111  symggen2  18112  psgnunilem1  18134  frgpnabllem2  18498  dprdss  18650  dprd2da  18663  dmdprdsplit2lem  18666  dpjidcl  18679  ablfac1b  18691  ablfac1eu  18694  isdrng2  18981  drngmcl  18984  drngid2  18987  isdrngd  18996  xrs1mnd  20012  xrs10  20013  xrs1cmn  20014  xrge0subm  20015  xrge0cmn  20016  cnmgpid  20036  cnmsubglem  20037  expghm  20072  cnmsgngrp  20152  psgninv  20155  dsmmfi  20313  islinds2  20383  lindsind2  20389  lindfrn  20391  islindf4  20408  mdetdiaglem  20636  mdetrsca2  20642  mdetrlin2  20645  mdetralt  20646  mdetunilem5  20654  mdetunilem9  20658  maducoeval2  20678  smadiadetglem1  20710  isopn2  21071  ntrval2  21090  ntrdif  21091  clsdif  21092  ntrss  21094  cmclsopn  21101  discld  21128  mretopd  21131  lpsscls  21180  restntr  21221  cmpcld  21440  2ndcsep  21497  1stccnp  21500  llycmpkgen2  21588  1stckgen  21592  txkgen  21690  qtopcld  21751  qtopcmap  21757  kqdisj  21770  isufil2  21946  ufileu  21957  filufint  21958  fixufil  21960  cfinufil  21966  ufilen  21968  fin1aufil  21970  supnfcls  22058  flimfnfcls  22066  alexsublem  22082  alexsubALTlem3  22087  cldsubg  22148  imasdsf1olem  22412  recld2  22851  sszcld  22854  xrge0gsumle  22870  divcn  22905  cdivcncf  22954  bcth3  23362  ismbl2  23531  cmmbl  23538  nulmbl  23539  nulmbl2  23540  unmbl  23541  voliunlem1  23554  voliunlem2  23555  ioombl1lem4  23565  ioombl1  23566  uniioombllem3  23589  mbfss  23650  itg1cl  23689  itg1ge0  23690  i1f0  23691  i1f1  23694  i1fmul  23700  itg1addlem4  23703  itg1mulc  23708  itg10a  23714  itg1ge0a  23715  itg1climres  23718  itg2cnlem1  23765  itgioo  23819  itgsplitioo  23841  limcdif  23877  ellimc2  23878  ellimc3  23880  limcflflem  23881  limcflf  23882  limcmo  23883  limcresi  23886  dvreslem  23910  dvres2lem  23911  dvidlem  23916  dvcnp2  23920  dvaddbr  23938  dvmulbr  23939  dvcobr  23946  dvrec  23955  dvcnvlem  23976  lhop1lem  24013  lhop  24016  tdeglem4  24057  deg1n0ima  24086  aacjcl  24319  taylthlem2  24365  abelth  24432  logcnlem5  24629  dvlog2  24636  efopnlem2  24640  dvcncxp1  24721  dvcnsqrt  24722  cxpcn2  24724  sqrtcn  24728  efrlim  24933  jensen  24952  amgm  24954  lgamgulmlem2  24993  lgamucov  25001  wilthlem2  25032  dchrelbas2  25199  rpvmasum2  25438  dchrisum0re  25439  dchrisum0lem3  25445  dchrisum0  25446  tgisline  25759  upgrss  26220  frgrwopreg2  27517  xrge00  30034  submatres  30220  madjusmdetlem2  30242  madjusmdetlem3  30243  qtophaus  30251  fsumcvg4  30344  gsumesum  30469  pwsiga  30541  sigainb  30547  carsggect  30728  omsmeas  30733  sitgclg  30752  ballotlemfelz  30900  ballotlemfp1  30901  ballotth  30947  cxpcncf1  31021  logdivsqrle  31076  hgt750lemb  31082  kur14lem6  31538  kur14lem7  31539  cvmscld  31600  mclsppslem  31825  fundmpss  32008  frpoind  32083  frind  32086  relsset  32338  limitssson  32361  fnsingle  32369  funimage  32378  cldbnd  32664  clsun  32666  topdifinffinlem  33530  matunitlindflem1  33737  poimirlem8  33749  poimirlem26  33767  poimirlem30  33771  mblfinlem3  33780  mblfinlem4  33781  ismblfin  33782  voliunnfl  33785  cnambfre  33789  dvtan  33791  dvasin  33827  dvacos  33828  areacirclem4  33834  fdc  33871  divrngcl  34086  isdrngo2  34087  isdrngo3  34088  islsati  34793  hdmap14lem2a  37666  istopclsd  37783  diophin  37856  dnnumch1  38133  cntzsdrg  38291  isdomn3  38301  deg1mhm  38304  gneispace  38950  sumnnodd  40360  cncficcgt0  40599  cncfiooicclem1  40604  cxpcncf2  40611  dirkercncflem2  40818  fourierdlem62  40882  fourierdlem66  40886  fourierdlem68  40888  fourierdlem95  40915  etransclem24  40972  etransclem44  40992  gsumge0cl  41085  sge0fodjrnlem  41130  carageniuncllem1  41235  smfresal  41495  lindslinindimp2lem2  42834  amgmlemALT  43138