Theorem difss 4102

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

Syntax hints:   ∖ cdif 3914   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934

This theorem is referenced by:  difssd  4103  difss2  4104  ssdifss  4106  0dif  4371  disj4  4425  difsnpss  4774  unidif  4909  iunxdif2  5020  difexg  5287  difelpw  5312  reldif  5781  cnvdif  6119  difxp  6140  frpoind  6318  tz7.7  6361  fresaun  6734  fresaunres2  6735  resdif  6824  fndmdif  7017  tfi  7832  peano5  7872  oelim2  8562  swoer  8705  swoord1  8706  swoord2  8707  ralxpmap  8872  boxcutc  8917  undom  9033  undomOLD  9034  domunsncan  9046  sbthlem2  9058  sbthlem4  9060  sbthlem5  9061  limenpsi  9122  diffi  9145  php3  9179  frfi  9239  fofinf1o  9290  ixpfi2  9308  elfiun  9388  marypha1lem  9391  wemapso  9511  infdifsn  9617  cantnflem2  9650  frind  9710  frr1  9719  dfac8alem  9989  acnnum  10012  inffien  10023  kmlem5  10115  infdif  10168  infdif2  10169  ackbij1lem18  10196  fictb  10204  fin23lem7  10276  fin23lem11  10277  fin23lem28  10300  fin23lem30  10302  compsscnvlem  10330  isf34lem2  10333  compssiso  10334  isf34lem4  10337  fin1a2lem7  10366  axcclem  10417  zornn0g  10465  ttukey2g  10476  pinn  10838  niex  10841  ltsopi  10848  dmaddpi  10850  dmmulpi  10851  lerelxr  11244  mulnzcnf  11831  dflt2  13115  expcl2lem  14045  expclzlem  14055  hashun2  14355  fsumss  15698  fsumless  15769  cvgcmpce  15791  fprodss  15921  rpnnen2lem9  16197  isstruct2  17126  structcnvcnv  17130  strleun  17134  strle1  17135  fsets  17146  mreexexlem2d  17613  gsumpropd2lem  18613  symgfixf1  19374  f1omvdmvd  19380  mvdco  19382  f1omvdconj  19383  pmtrfb  19402  pmtrfconj  19403  symggen  19407  symggen2  19408  psgnunilem1  19430  frgpnabllem2  19811  dprdss  19968  dprd2da  19981  dmdprdsplit2lem  19984  dpjidcl  19997  ablfac1b  20009  ablfac1eu  20012  isdomn3  20631  isdrng2  20659  drngmclOLD  20667  drngid2  20668  isdrngd  20681  isdrngdOLD  20683  cntzsdrg  20718  subdrgint  20719  xrs1mnd  21328  xrs10  21329  xrs1cmn  21330  xrge0subm  21331  xrge0cmn  21332  cnmgpid  21353  cnmsubglem  21354  expghm  21392  dsmmfi  21654  islinds2  21729  lindsind2  21735  lindfrn  21737  islindf4  21754  psdmul  22060  mdetdiaglem  22492  mdetrsca2  22498  mdetrlin2  22501  mdetralt  22502  mdetunilem5  22510  mdetunilem9  22514  maducoeval2  22534  smadiadetglem1  22565  isopn2  22926  ntrval2  22945  ntrdif  22946  clsdif  22947  ntrss  22949  cmclsopn  22956  discld  22983  mretopd  22986  lpsscls  23035  restntr  23076  cmpcld  23296  2ndcsep  23353  1stccnp  23356  llycmpkgen2  23444  1stckgen  23448  txkgen  23546  qtopcld  23607  qtopcmap  23613  kqdisj  23626  isufil2  23802  ufileu  23813  filufint  23814  fixufil  23816  cfinufil  23822  ufilen  23824  fin1aufil  23826  supnfcls  23914  flimfnfcls  23922  alexsublem  23938  alexsubALTlem3  23943  cldsubg  24005  imasdsf1olem  24268  recld2  24710  sszcld  24713  xrge0gsumle  24729  divcnOLD  24764  divcn  24766  cdivcncf  24821  bcth3  25238  ismbl2  25435  cmmbl  25442  nulmbl  25443  nulmbl2  25444  unmbl  25445  voliunlem1  25458  voliunlem2  25459  ioombl1lem4  25469  ioombl1  25470  uniioombllem3  25493  mbfss  25554  itg1cl  25593  itg1ge0  25594  i1f0  25595  i1f1  25598  i1fmul  25604  itg1addlem4  25607  itg1mulc  25612  itg10a  25618  itg1ge0a  25619  itg1climres  25622  itg2cnlem1  25669  itgioo  25724  itgsplitioo  25746  limcdif  25784  ellimc2  25785  ellimc3  25787  limcflflem  25788  limcflf  25789  limcmo  25790  limcresi  25793  dvreslem  25817  dvres2lem  25818  dvidlem  25823  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  dvrec  25866  dvcnvlem  25887  lhop1lem  25925  lhop  25928  tdeglem4  25972  deg1n0ima  26001  aacjcl  26242  taylthlem2  26289  taylthlem2OLD  26290  abelth  26358  logcnlem5  26562  dvlog2  26569  efopnlem2  26573  dvcncxp1  26659  dvcnsqrt  26660  cxpcn2  26663  sqrtcn  26667  efrlim  26886  efrlimOLD  26887  jensen  26906  amgm  26908  lgamgulmlem2  26947  lgamucov  26955  wilthlem2  26986  dchrelbas2  27155  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem3  27437  dchrisum0  27438  nnssn0s  28221  tgisline  28561  upgrss  29022  frgrwopreg2  30255  difxp1ss  32458  difxp2ss  32459  xrge00  32960  symgcom2  33048  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  cycpmrn  33107  tocyccntz  33108  submatres  33803  madjusmdetlem2  33825  madjusmdetlem3  33826  qtophaus  33833  fsumcvg4  33947  gsumesum  34056  pwsiga  34127  sigainb  34133  carsggect  34316  omsmeas  34321  sitgclg  34340  ballotlemfelz  34489  ballotlemfp1  34490  ballotth  34536  cxpcncf1  34593  logdivsqrle  34648  hgt750lemb  34654  kur14lem6  35205  kur14lem7  35206  cvmscld  35267  satfvsucsuc  35359  satfrnmapom  35364  mclsppslem  35577  fundmpss  35761  relsset  35883  limitssson  35906  fnsingle  35914  funimage  35923  cldbnd  36321  clsun  36323  topdifinffinlem  37342  inunissunidif  37370  pibt2  37412  matunitlindflem1  37617  poimirlem8  37629  poimirlem26  37647  poimirlem30  37651  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  voliunnfl  37665  cnambfre  37669  dvtan  37671  dvasin  37705  dvacos  37706  areacirclem4  37712  fdc  37746  divrngcl  37958  isdrngo2  37959  isdrngo3  37960  islsati  38994  hdmap14lem2a  41868  redvmptabs  42355  prjspreln0  42604  prjspvs  42605  prjspeclsp  42607  0prjspnrel  42622  istopclsd  42695  diophin  42767  dnnumch1  43040  deg1mhm  43196  gneispace  44130  inaex  44293  sumnnodd  45635  cncficcgt0  45893  cncfiooicclem1  45898  cxpcncf2  45904  dirkercncflem2  46109  fourierdlem62  46173  fourierdlem66  46177  fourierdlem68  46179  fourierdlem95  46206  etransclem24  46263  etransclem44  46283  gsumge0cl  46376  sge0fodjrnlem  46421  carageniuncllem1  46526  smfresal  46793  dfnbgrss  47856  dfnbgrss2  47863  lindslinindimp2lem2  48452  iscnrm3rlem2  48933  amgmlemALT  49796