Theorem difss 4111

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

Syntax hints:   ∖ cdif 3923   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943

This theorem is referenced by:  difssd  4112  difss2  4113  ssdifss  4115  0dif  4380  disj4  4434  difsnpss  4783  unidif  4918  iunxdif2  5029  difexg  5299  difelpw  5324  reldif  5794  cnvdif  6132  difxp  6153  frpoind  6331  wfiOLD  6340  tz7.7  6378  fresaun  6748  fresaunres2  6749  resdif  6838  fndmdif  7031  tfi  7846  peano5  7887  wfrlem16OLD  8336  oelim2  8605  swoer  8748  swoord1  8749  swoord2  8750  ralxpmap  8908  boxcutc  8953  undom  9071  undomOLD  9072  domunsncan  9084  sbthlem2  9096  sbthlem4  9098  sbthlem5  9099  limenpsi  9164  diffi  9187  php3  9221  phplem2OLD  9227  php3OLD  9231  frfi  9291  fofinf1o  9342  ixpfi2  9360  elfiun  9440  marypha1lem  9443  wemapso  9563  infdifsn  9669  cantnflem2  9702  frind  9762  frr1  9771  dfac8alem  10041  acnnum  10064  inffien  10075  kmlem5  10167  infdif  10220  infdif2  10221  ackbij1lem18  10248  fictb  10256  fin23lem7  10328  fin23lem11  10329  fin23lem28  10352  fin23lem30  10354  compsscnvlem  10382  isf34lem2  10385  compssiso  10386  isf34lem4  10389  fin1a2lem7  10418  axcclem  10469  zornn0g  10517  ttukey2g  10528  pinn  10890  niex  10893  ltsopi  10900  dmaddpi  10902  dmmulpi  10903  lerelxr  11296  mulnzcnf  11881  dflt2  13162  expcl2lem  14089  expclzlem  14099  hashun2  14399  fsumss  15739  fsumless  15810  cvgcmpce  15832  fprodss  15962  rpnnen2lem9  16238  isstruct2  17166  structcnvcnv  17170  strleun  17174  strle1  17175  fsets  17186  mreexexlem2d  17655  gsumpropd2lem  18655  symgfixf1  19416  f1omvdmvd  19422  mvdco  19424  f1omvdconj  19425  pmtrfb  19444  pmtrfconj  19445  symggen  19449  symggen2  19450  psgnunilem1  19472  frgpnabllem2  19853  dprdss  20010  dprd2da  20023  dmdprdsplit2lem  20026  dpjidcl  20039  ablfac1b  20051  ablfac1eu  20054  isdomn3  20673  isdrng2  20701  drngmclOLD  20709  drngid2  20710  isdrngd  20723  isdrngdOLD  20725  cntzsdrg  20760  subdrgint  20761  xrs1mnd  21370  xrs10  21371  xrs1cmn  21372  xrge0subm  21373  xrge0cmn  21374  cnmgpid  21395  cnmsubglem  21396  expghm  21434  dsmmfi  21696  islinds2  21771  lindsind2  21777  lindfrn  21779  islindf4  21796  psdmul  22102  mdetdiaglem  22534  mdetrsca2  22540  mdetrlin2  22543  mdetralt  22544  mdetunilem5  22552  mdetunilem9  22556  maducoeval2  22576  smadiadetglem1  22607  isopn2  22968  ntrval2  22987  ntrdif  22988  clsdif  22989  ntrss  22991  cmclsopn  22998  discld  23025  mretopd  23028  lpsscls  23077  restntr  23118  cmpcld  23338  2ndcsep  23395  1stccnp  23398  llycmpkgen2  23486  1stckgen  23490  txkgen  23588  qtopcld  23649  qtopcmap  23655  kqdisj  23668  isufil2  23844  ufileu  23855  filufint  23856  fixufil  23858  cfinufil  23864  ufilen  23866  fin1aufil  23868  supnfcls  23956  flimfnfcls  23964  alexsublem  23980  alexsubALTlem3  23985  cldsubg  24047  imasdsf1olem  24310  recld2  24752  sszcld  24755  xrge0gsumle  24771  divcnOLD  24806  divcn  24808  cdivcncf  24863  bcth3  25281  ismbl2  25478  cmmbl  25485  nulmbl  25486  nulmbl2  25487  unmbl  25488  voliunlem1  25501  voliunlem2  25502  ioombl1lem4  25512  ioombl1  25513  uniioombllem3  25536  mbfss  25597  itg1cl  25636  itg1ge0  25637  i1f0  25638  i1f1  25641  i1fmul  25647  itg1addlem4  25650  itg1mulc  25655  itg10a  25661  itg1ge0a  25662  itg1climres  25665  itg2cnlem1  25712  itgioo  25767  itgsplitioo  25789  limcdif  25827  ellimc2  25828  ellimc3  25830  limcflflem  25831  limcflf  25832  limcmo  25833  limcresi  25836  dvreslem  25860  dvres2lem  25861  dvidlem  25866  dvcnp2  25871  dvcnp2OLD  25872  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcobr  25899  dvcobrOLD  25900  dvrec  25909  dvcnvlem  25930  lhop1lem  25968  lhop  25971  tdeglem4  26015  deg1n0ima  26044  aacjcl  26285  taylthlem2  26332  taylthlem2OLD  26333  abelth  26401  logcnlem5  26605  dvlog2  26612  efopnlem2  26616  dvcncxp1  26702  dvcnsqrt  26703  cxpcn2  26706  sqrtcn  26710  efrlim  26929  efrlimOLD  26930  jensen  26949  amgm  26951  lgamgulmlem2  26990  lgamucov  26998  wilthlem2  27029  dchrelbas2  27198  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem3  27480  dchrisum0  27481  nnssn0s  28243  tgisline  28552  upgrss  29013  frgrwopreg2  30246  difxp1ss  32449  difxp2ss  32450  xrge00  32953  symgcom2  33041  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  cycpmrn  33100  tocyccntz  33101  submatres  33783  madjusmdetlem2  33805  madjusmdetlem3  33806  qtophaus  33813  fsumcvg4  33927  gsumesum  34036  pwsiga  34107  sigainb  34113  carsggect  34296  omsmeas  34301  sitgclg  34320  ballotlemfelz  34469  ballotlemfp1  34470  ballotth  34516  cxpcncf1  34573  logdivsqrle  34628  hgt750lemb  34634  kur14lem6  35179  kur14lem7  35180  cvmscld  35241  satfvsucsuc  35333  satfrnmapom  35338  mclsppslem  35551  fundmpss  35730  relsset  35852  limitssson  35875  fnsingle  35883  funimage  35892  cldbnd  36290  clsun  36292  topdifinffinlem  37311  inunissunidif  37339  pibt2  37381  matunitlindflem1  37586  poimirlem8  37598  poimirlem26  37616  poimirlem30  37620  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  voliunnfl  37634  cnambfre  37638  dvtan  37640  dvasin  37674  dvacos  37675  areacirclem4  37681  fdc  37715  divrngcl  37927  isdrngo2  37928  isdrngo3  37929  islsati  38958  hdmap14lem2a  41832  redvmptabs  42350  prjspreln0  42579  prjspvs  42580  prjspeclsp  42582  0prjspnrel  42597  istopclsd  42670  diophin  42742  dnnumch1  43015  deg1mhm  43171  gneispace  44105  inaex  44269  sumnnodd  45607  cncficcgt0  45865  cncfiooicclem1  45870  cxpcncf2  45876  dirkercncflem2  46081  fourierdlem62  46145  fourierdlem66  46149  fourierdlem68  46151  fourierdlem95  46178  etransclem24  46235  etransclem44  46255  gsumge0cl  46348  sge0fodjrnlem  46393  carageniuncllem1  46498  smfresal  46765  dfnbgrss  47813  dfnbgrss2  47820  lindslinindimp2lem2  48383  iscnrm3rlem2  48863  amgmlemALT  49615