Theorem difss 4110

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

Syntax hints:   ∖ cdif 3935   ⊆ wss 3938

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954

This theorem is referenced by:  difssd  4111  difss2  4112  ssdifss  4114  0dif  4357  disj4  4410  difsnpss  4742  unidif  4874  iunxdif2  4979  difexg  5233  difelpw  5254  reldif  5690  cnvdif  6004  difxp  6023  wfi  6183  tz7.7  6219  fresaun  6551  fresaunres2  6552  resdif  6637  fndmdif  6814  tfi  7570  peano5  7607  wfrlem16  7972  oelim2  8223  swoer  8321  swoord1  8322  swoord2  8323  ralxpmap  8462  boxcutc  8507  undom  8607  domunsncan  8619  sbthlem2  8630  sbthlem4  8632  sbthlem5  8633  limenpsi  8694  phplem2  8699  php3  8705  diffi  8752  frfi  8765  fofinf1o  8801  ixpfi2  8824  elfiun  8896  marypha1lem  8899  wemapso  9017  infdifsn  9122  cantnflem2  9155  dfac8alem  9457  acnnum  9480  inffien  9491  kmlem5  9582  infdif  9633  infdif2  9634  ackbij1lem18  9661  fictb  9669  fin23lem7  9740  fin23lem11  9741  fin23lem28  9764  fin23lem30  9766  compsscnvlem  9794  isf34lem2  9797  compssiso  9798  isf34lem4  9801  fin1a2lem7  9830  axcclem  9881  zornn0g  9929  ttukey2g  9940  pinn  10302  niex  10305  ltsopi  10312  dmaddpi  10314  dmmulpi  10315  lerelxr  10706  mulnzcnopr  11288  dflt2  12544  expcl2lem  13444  expclzlem  13456  hashun2  13747  fsumss  15084  fsumless  15153  cvgcmpce  15175  fprodss  15304  rpnnen2lem9  15577  isstruct2  16495  structcnvcnv  16499  fsets  16518  strleun  16593  strle1  16594  mreexexlem2d  16918  gsumpropd2lem  17891  symgfixf1  18567  f1omvdmvd  18573  mvdco  18575  f1omvdconj  18576  pmtrfb  18595  pmtrfconj  18596  symggen  18600  symggen2  18601  psgnunilem1  18623  frgpnabllem2  18996  dprdss  19153  dprd2da  19166  dmdprdsplit2lem  19169  dpjidcl  19182  ablfac1b  19194  ablfac1eu  19197  isdrng2  19514  drngmcl  19517  drngid2  19520  isdrngd  19529  cntzsdrg  19583  subdrgint  19584  xrs1mnd  20585  xrs10  20586  xrs1cmn  20587  xrge0subm  20588  xrge0cmn  20589  cnmgpid  20609  cnmsubglem  20610  expghm  20645  dsmmfi  20884  islinds2  20959  lindsind2  20965  lindfrn  20967  islindf4  20984  mdetdiaglem  21209  mdetrsca2  21215  mdetrlin2  21218  mdetralt  21219  mdetunilem5  21227  mdetunilem9  21231  maducoeval2  21251  smadiadetglem1  21282  isopn2  21642  ntrval2  21661  ntrdif  21662  clsdif  21663  ntrss  21665  cmclsopn  21672  discld  21699  mretopd  21702  lpsscls  21751  restntr  21792  cmpcld  22012  2ndcsep  22069  1stccnp  22072  llycmpkgen2  22160  1stckgen  22164  txkgen  22262  qtopcld  22323  qtopcmap  22329  kqdisj  22342  isufil2  22518  ufileu  22529  filufint  22530  fixufil  22532  cfinufil  22538  ufilen  22540  fin1aufil  22542  supnfcls  22630  flimfnfcls  22638  alexsublem  22654  alexsubALTlem3  22659  cldsubg  22721  imasdsf1olem  22985  recld2  23424  sszcld  23427  xrge0gsumle  23443  divcn  23478  cdivcncf  23527  bcth3  23936  ismbl2  24130  cmmbl  24137  nulmbl  24138  nulmbl2  24139  unmbl  24140  voliunlem1  24153  voliunlem2  24154  ioombl1lem4  24164  ioombl1  24165  uniioombllem3  24188  mbfss  24249  itg1cl  24288  itg1ge0  24289  i1f0  24290  i1f1  24293  i1fmul  24299  itg1addlem4  24302  itg1mulc  24307  itg10a  24313  itg1ge0a  24314  itg1climres  24317  itg2cnlem1  24364  itgioo  24418  itgsplitioo  24440  limcdif  24476  ellimc2  24477  ellimc3  24479  limcflflem  24480  limcflf  24481  limcmo  24482  limcresi  24485  dvreslem  24509  dvres2lem  24510  dvidlem  24515  dvcnp2  24519  dvaddbr  24537  dvmulbr  24538  dvcobr  24545  dvrec  24554  dvcnvlem  24575  lhop1lem  24612  lhop  24615  tdeglem4  24656  deg1n0ima  24685  aacjcl  24918  taylthlem2  24964  abelth  25031  logcnlem5  25231  dvlog2  25238  efopnlem2  25242  dvcncxp1  25326  dvcnsqrt  25327  cxpcn2  25329  sqrtcn  25333  efrlim  25549  jensen  25568  amgm  25570  lgamgulmlem2  25609  lgamucov  25617  wilthlem2  25648  dchrelbas2  25815  rpvmasum2  26090  dchrisum0re  26091  dchrisum0lem3  26097  dchrisum0  26098  tgisline  26415  upgrss  26875  frgrwopreg2  28100  difxp1ss  30284  difxp2ss  30285  xrge00  30675  symgcom2  30730  pmtrcnel  30735  pmtrcnel2  30736  pmtrcnelor  30737  cycpmrn  30787  tocyccntz  30788  submatres  31073  madjusmdetlem2  31095  madjusmdetlem3  31096  qtophaus  31102  fsumcvg4  31195  gsumesum  31320  pwsiga  31391  sigainb  31397  carsggect  31578  omsmeas  31583  sitgclg  31602  ballotlemfelz  31750  ballotlemfp1  31751  ballotth  31797  cxpcncf1  31868  logdivsqrle  31923  hgt750lemb  31929  kur14lem6  32460  kur14lem7  32461  cvmscld  32522  satfvsucsuc  32614  satfrnmapom  32619  mclsppslem  32832  fundmpss  33011  frpoind  33082  frind  33087  frr1  33146  relsset  33351  limitssson  33374  fnsingle  33382  funimage  33391  cldbnd  33676  clsun  33678  topdifinffinlem  34630  inunissunidif  34658  pibt2  34700  matunitlindflem1  34890  poimirlem8  34902  poimirlem26  34920  poimirlem30  34924  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  voliunnfl  34938  cnambfre  34942  dvtan  34944  dvasin  34980  dvacos  34981  areacirclem4  34987  fdc  35022  divrngcl  35237  isdrngo2  35238  isdrngo3  35239  islsati  36132  hdmap14lem2a  39005  prjspreln0  39266  prjspvs  39267  prjspeclsp  39269  0prjspnrel  39276  istopclsd  39304  diophin  39376  dnnumch1  39651  isdomn3  39811  deg1mhm  39814  gneispace  40491  inaex  40640  sumnnodd  41918  cncficcgt0  42178  cncfiooicclem1  42183  cxpcncf2  42190  dirkercncflem2  42396  fourierdlem62  42460  fourierdlem66  42464  fourierdlem68  42466  fourierdlem95  42493  etransclem24  42550  etransclem44  42570  gsumge0cl  42660  sge0fodjrnlem  42705  carageniuncllem1  42810  smfresal  43070  lindslinindimp2lem2  44521  amgmlemALT  44911