Theorem difss 4083

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

This proof depends on syntax axioms:   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916

This theorem is used by:  difssd  4084  difss2  4085  ssdifss  4087  0dif  4356  disj4  4412  difsnpss  4770  unidif  4903  iunxdif2  5012  difexg  5291  difelpw  5315  reldif  5793  cnvdif  6134  difxp  6155  frpoind  6344  tz7.7  6387  fresaun  6751  fresaunres2  6752  resdif  6844  fndmdif  7039  tfi  7862  peano5  7903  oelim2  8597  swoer  8742  swoord1  8743  swoord2  8744  ralxpmap  8917  boxcutc  8962  undom  9077  domunsncan  9089  sbthlem2  9100  sbthlem4  9102  sbthlem5  9103  limenpsi  9164  diffi  9183  php3  9217  frfi  9269  fofinf1o  9314  ixpfi2  9332  elfiun  9415  marypha1lem  9418  wemapso  9538  infdifsn  9651  cantnflem2  9684  frind  9747  frr1  9756  dfac8alem  10101  acnnum  10124  inffien  10135  kmlem5  10226  infdif  10279  infdif2  10280  ackbij1lem18  10307  fictb  10315  fin23lem7  10387  fin23lem11  10388  fin23lem28  10411  fin23lem30  10413  compsscnvlem  10441  isf34lem2  10444  compssiso  10445  isf34lem4  10448  fin1a2lem7  10477  axcclem  10528  zornn0g  10576  ttukey2g  10587  pinn  10956  niex  10959  ltsopi  10966  dmaddpi  10968  dmmulpi  10969  lerelxr  11365  mulnzcnf  11955  dflt2  13270  expcl2lem  14209  expclzlem  14219  hashun2  14520  fsumss  15884  fsumless  15956  cvgcmpce  15978  fprodss  16108  rpnnen2lem9  16383  isstruct2  17320  structcnvcnv  17324  strleun  17328  strle1  17329  fsets  17340  mreexexlem2d  17812  gsumpropd2lem  18861  symgfixf1  19644  f1omvdmvd  19650  mvdco  19652  f1omvdconj  19653  pmtrfb  19672  pmtrfconj  19673  symggen  19677  symggen2  19678  psgnunilem1  19700  frgpnabllem2  20081  dprdss  20238  dprd2da  20251  dmdprdsplit2lem  20254  dpjidcl  20267  ablfac1b  20279  ablfac1eu  20282  isdomn3  20959  isdrng2  20990  isdrng3lem0  20997  isdrng3lem2  20999  isdrng5  21001  drngid2  21003  isdrngd  21015  isdrngdOLD  21017  cntzsdrg  21052  subdrgint  21053  prmidlsubm  21636  cnmgpid  21728  cnmsubglem  21729  xrs1mnd  21739  xrs10  21740  xrs1cmn  21741  xrge0subm  21742  xrge0cmn  21743  expghm  21774  dsmmfi  22037  islinds2  22112  lindsind2  22118  lindfrn  22120  islindf4  22137  psdmul  22480  mdetdiaglem  22906  mdetrsca2  22912  mdetrlin2  22915  mdetralt  22916  mdetunilem5  22924  mdetunilem9  22928  maducoeval2  22948  smadiadetglem1  22979  matunitlindflem1  22987  isopn2  23343  ntrval2  23362  ntrdif  23363  clsdif  23364  ntrss  23366  cmclsopn  23373  discld  23400  mretopd  23403  lpsscls  23452  restntr  23493  cmpcld  23713  2ndcsep  23771  1stccnp  23774  llycmpkgen2  23862  1stckgen  23866  txkgen  23964  qtopcld  24025  qtopcmap  24031  kqdisj  24044  isufil2  24220  ufileu  24231  filufint  24232  fixufil  24234  cfinufil  24240  ufilen  24242  fin1aufil  24244  supnfcls  24332  flimfnfcls  24340  alexsublem  24356  alexsubALTlem3  24361  cldsubg  24423  imasdsf1olem  24685  recld2  25127  sszcld  25130  xrge0gsumle  25146  divcn  25182  cdivcncf  25235  bcth3  25645  ismbl2  25841  cmmbl  25848  nulmbl  25849  nulmbl2  25850  unmbl  25851  voliunlem1  25864  voliunlem2  25865  ioombl1lem4  25875  ioombl1  25876  uniioombllem3  25899  mbfss  25960  itg1cl  25999  itg1ge0  26000  i1f0  26001  i1f1  26004  i1fmul  26010  itg1addlem4  26013  itg1mulc  26018  itg10a  26024  itg1ge0a  26025  itg1climres  26028  itg2cnlem1  26075  itgioo  26129  itgsplitioo  26151  limcdif  26189  ellimc2  26190  ellimc3  26192  limcflflem  26193  limcflf  26194  limcmo  26195  limcresi  26198  dvreslem  26222  dvres2lem  26223  dvidlem  26228  dvcnp2  26233  dvaddbr  26251  dvmulbr  26252  dvcobr  26259  dvrec  26268  dvcnvlem  26289  lhop1lem  26326  lhop  26329  tdeglem4  26371  deg1n0ima  26400  aacjcl  26647  taylthlem2  26694  abelth  26761  logcnlem5  26967  dvlog2  26974  efopnlem2  26978  dvcncxp1  27064  dvcnsqrt  27065  cxpcn2  27067  sqrtcn  27071  efrlim  27290  jensen  27309  amgm  27311  lgamgulmlem2  27350  lgamucov  27358  wilthlem2  27389  dchrelbas2  27557  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lem3  27839  dchrisum0  27840  nnssn0s  28700  tgisline  29088  upgrss  29659  frgrwopreg2  30913  difxp1ss  33111  difxp2ss  33112  xrge00  33568  symgcom2  33638  pmtrcnel  33643  pmtrcnel2  33644  pmtrcnelor  33645  cycpmrn  33697  tocyccntz  33698  evlextv  34167  vietalem  34204  submatres  34431  madjusmdetlem2  34453  madjusmdetlem3  34454  qtophaus  34461  fsumcvg4  34575  gsumesum  34684  pwsiga  34755  sigainb  34762  carsggect  34943  omsmeas  34948  sitgclg  34967  ballotlemfelz  35116  ballotlemfp1  35117  ballotth  35163  cxpcncf1  35217  logdivsqrle  35272  hgt750lemb  35278  fineqvnttrclse  35775  kur14lem6  35955  kur14lem7  35956  cvmscld  36017  satfvsucsuc  36109  satfrnmapom  36114  mclsppslem  36327  fundmpss  36511  relsset  36630  limitssson  36653  fnsingle  36661  funimage  36670  cldbnd  37094  clsun  37096  topdifinffinlem  38250  inunissunidif  38278  pibt2  38320  poimirlem8  38526  poimirlem26  38544  poimirlem30  38548  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  voliunnfl  38562  cnambfre  38566  dvtan  38568  dvasin  38602  dvacos  38603  areacirclem4  38609  fdc  38659  divrngcl  38871  isdrngo2  38872  isdrngo3  38873  islsati  40031  hdmap14lem2a  42904  redvmptabs  43391  prjspreln0  43617  prjspvs  43618  prjspeclsp  43620  frlmnzcoordcl2  43636  prjspnnorm  43641  0prjspnrel  43643  istopclsd  43690  diophin  43762  dnnumch1  44030  deg1mhm  44186  gneispace  45119  inaex  45266  sumnnodd  46611  cncficcgt0  46867  cncfiooicclem1  46872  cxpcncf2  46878  dirkercncflem2  47083  fourierdlem62  47147  fourierdlem66  47151  fourierdlem68  47153  fourierdlem95  47180  etransclem24  47237  etransclem44  47257  gsumge0cl  47350  sge0fodjrnlem  47395  carageniuncllem1  47500  smfresal  47767  dfnbgrss  48919  dfnbgrss2  48926  lindslinindimp2lem2  49540  iscnrm3rlem2  50018  amgmlemALT  50957