Theorem difss 4159

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

Syntax hints:   ∖ cdif 3973   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993

This theorem is referenced by:  difssd  4160  difss2  4161  ssdifss  4163  0dif  4428  disj4  4482  difsnpss  4832  unidif  4966  iunxdif2  5076  difexg  5347  difelpw  5372  reldif  5839  cnvdif  6175  difxp  6195  frpoind  6374  wfiOLD  6383  tz7.7  6421  fresaun  6792  fresaunres2  6793  resdif  6883  fndmdif  7075  tfi  7890  peano5  7932  peano5OLD  7933  wfrlem16OLD  8380  oelim2  8651  swoer  8794  swoord1  8795  swoord2  8796  ralxpmap  8954  boxcutc  8999  undom  9125  undomOLD  9126  domunsncan  9138  sbthlem2  9150  sbthlem4  9152  sbthlem5  9153  limenpsi  9218  diffi  9242  php3  9275  phplem2OLD  9281  php3OLD  9287  frfi  9349  fofinf1o  9400  ixpfi2  9420  elfiun  9499  marypha1lem  9502  wemapso  9620  infdifsn  9726  cantnflem2  9759  frind  9819  frr1  9828  dfac8alem  10098  acnnum  10121  inffien  10132  kmlem5  10224  infdif  10277  infdif2  10278  ackbij1lem18  10305  fictb  10313  fin23lem7  10385  fin23lem11  10386  fin23lem28  10409  fin23lem30  10411  compsscnvlem  10439  isf34lem2  10442  compssiso  10443  isf34lem4  10446  fin1a2lem7  10475  axcclem  10526  zornn0g  10574  ttukey2g  10585  pinn  10947  niex  10950  ltsopi  10957  dmaddpi  10959  dmmulpi  10960  lerelxr  11353  mulnzcnf  11936  dflt2  13210  expcl2lem  14124  expclzlem  14134  hashun2  14432  fsumss  15773  fsumless  15844  cvgcmpce  15866  fprodss  15996  rpnnen2lem9  16270  isstruct2  17196  structcnvcnv  17200  strleun  17204  strle1  17205  fsets  17216  mreexexlem2d  17703  gsumpropd2lem  18717  symgfixf1  19479  f1omvdmvd  19485  mvdco  19487  f1omvdconj  19488  pmtrfb  19507  pmtrfconj  19508  symggen  19512  symggen2  19513  psgnunilem1  19535  frgpnabllem2  19916  dprdss  20073  dprd2da  20086  dmdprdsplit2lem  20089  dpjidcl  20102  ablfac1b  20114  ablfac1eu  20117  isdomn3  20737  isdrng2  20765  drngmclOLD  20773  drngid2  20774  isdrngd  20787  isdrngdOLD  20789  cntzsdrg  20825  subdrgint  20826  xrs1mnd  21445  xrs10  21446  xrs1cmn  21447  xrge0subm  21448  xrge0cmn  21449  cnmgpid  21470  cnmsubglem  21471  expghm  21509  dsmmfi  21781  islinds2  21856  lindsind2  21862  lindfrn  21864  islindf4  21881  psdmul  22193  mdetdiaglem  22625  mdetrsca2  22631  mdetrlin2  22634  mdetralt  22635  mdetunilem5  22643  mdetunilem9  22647  maducoeval2  22667  smadiadetglem1  22698  isopn2  23061  ntrval2  23080  ntrdif  23081  clsdif  23082  ntrss  23084  cmclsopn  23091  discld  23118  mretopd  23121  lpsscls  23170  restntr  23211  cmpcld  23431  2ndcsep  23488  1stccnp  23491  llycmpkgen2  23579  1stckgen  23583  txkgen  23681  qtopcld  23742  qtopcmap  23748  kqdisj  23761  isufil2  23937  ufileu  23948  filufint  23949  fixufil  23951  cfinufil  23957  ufilen  23959  fin1aufil  23961  supnfcls  24049  flimfnfcls  24057  alexsublem  24073  alexsubALTlem3  24078  cldsubg  24140  imasdsf1olem  24404  recld2  24855  sszcld  24858  xrge0gsumle  24874  divcnOLD  24909  divcn  24911  cdivcncf  24966  bcth3  25384  ismbl2  25581  cmmbl  25588  nulmbl  25589  nulmbl2  25590  unmbl  25591  voliunlem1  25604  voliunlem2  25605  ioombl1lem4  25615  ioombl1  25616  uniioombllem3  25639  mbfss  25700  itg1cl  25739  itg1ge0  25740  i1f0  25741  i1f1  25744  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  itg1mulc  25759  itg10a  25765  itg1ge0a  25766  itg1climres  25769  itg2cnlem1  25816  itgioo  25871  itgsplitioo  25893  limcdif  25931  ellimc2  25932  ellimc3  25934  limcflflem  25935  limcflf  25936  limcmo  25937  limcresi  25940  dvreslem  25964  dvres2lem  25965  dvidlem  25970  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvrec  26013  dvcnvlem  26034  lhop1lem  26072  lhop  26075  tdeglem4  26119  deg1n0ima  26148  aacjcl  26387  taylthlem2  26434  taylthlem2OLD  26435  abelth  26503  logcnlem5  26706  dvlog2  26713  efopnlem2  26717  dvcncxp1  26803  dvcnsqrt  26804  cxpcn2  26807  sqrtcn  26811  efrlim  27030  efrlimOLD  27031  jensen  27050  amgm  27052  lgamgulmlem2  27091  lgamucov  27099  wilthlem2  27130  dchrelbas2  27299  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem3  27581  dchrisum0  27582  nnssn0s  28344  tgisline  28653  upgrss  29123  frgrwopreg2  30351  difxp1ss  32552  difxp2ss  32553  xrge00  32998  symgcom2  33077  pmtrcnel  33082  pmtrcnel2  33083  pmtrcnelor  33084  cycpmrn  33136  tocyccntz  33137  submatres  33752  madjusmdetlem2  33774  madjusmdetlem3  33775  qtophaus  33782  fsumcvg4  33896  gsumesum  34023  pwsiga  34094  sigainb  34100  carsggect  34283  omsmeas  34288  sitgclg  34307  ballotlemfelz  34455  ballotlemfp1  34456  ballotth  34502  cxpcncf1  34572  logdivsqrle  34627  hgt750lemb  34633  kur14lem6  35179  kur14lem7  35180  cvmscld  35241  satfvsucsuc  35333  satfrnmapom  35338  mclsppslem  35551  fundmpss  35730  relsset  35852  limitssson  35875  fnsingle  35883  funimage  35892  cldbnd  36292  clsun  36294  topdifinffinlem  37313  inunissunidif  37341  pibt2  37383  matunitlindflem1  37576  poimirlem8  37588  poimirlem26  37606  poimirlem30  37610  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  voliunnfl  37624  cnambfre  37628  dvtan  37630  dvasin  37664  dvacos  37665  areacirclem4  37671  fdc  37705  divrngcl  37917  isdrngo2  37918  isdrngo3  37919  islsati  38950  hdmap14lem2a  41824  prjspreln0  42564  prjspvs  42565  prjspeclsp  42567  0prjspnrel  42582  istopclsd  42656  diophin  42728  dnnumch1  43001  deg1mhm  43161  gneispace  44096  inaex  44266  sumnnodd  45551  cncficcgt0  45809  cncfiooicclem1  45814  cxpcncf2  45820  dirkercncflem2  46025  fourierdlem62  46089  fourierdlem66  46093  fourierdlem68  46095  fourierdlem95  46122  etransclem24  46179  etransclem44  46199  gsumge0cl  46292  sge0fodjrnlem  46337  carageniuncllem1  46442  smfresal  46709  dfnbgrss  47724  dfnbgrss2  47731  lindslinindimp2lem2  48188  iscnrm3rlem2  48621  amgmlemALT  48897