Theorem difss 4032

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

Syntax hints:   ∖ cdif 3850   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-in 3860  df-ss 3870

This theorem is referenced by:  difssd  4033  difss2  4034  ssdifss  4036  0dif  4302  disj4  4359  difsnpss  4706  unidif  4841  iunxdif2  4948  difexg  5205  difelpw  5228  reldif  5670  cnvdif  5987  difxp  6007  frpoind  6174  wfi  6181  tz7.7  6217  fresaun  6568  fresaunres2  6569  resdif  6659  fndmdif  6840  tfi  7610  peano5  7649  peano5OLD  7650  wfrlem16  8048  oelim2  8301  swoer  8399  swoord1  8400  swoord2  8401  ralxpmap  8555  boxcutc  8600  undom  8711  domunsncan  8723  sbthlem2  8735  sbthlem4  8737  sbthlem5  8738  limenpsi  8799  phplem2  8804  php3  8810  diffi  8884  frfi  8894  fofinf1o  8929  ixpfi2  8952  elfiun  9024  marypha1lem  9027  wemapso  9145  infdifsn  9250  cantnflem2  9283  dfac8alem  9608  acnnum  9631  inffien  9642  kmlem5  9733  infdif  9788  infdif2  9789  ackbij1lem18  9816  fictb  9824  fin23lem7  9895  fin23lem11  9896  fin23lem28  9919  fin23lem30  9921  compsscnvlem  9949  isf34lem2  9952  compssiso  9953  isf34lem4  9956  fin1a2lem7  9985  axcclem  10036  zornn0g  10084  ttukey2g  10095  pinn  10457  niex  10460  ltsopi  10467  dmaddpi  10469  dmmulpi  10470  lerelxr  10861  mulnzcnopr  11443  dflt2  12703  expcl2lem  13612  expclzlem  13624  hashun2  13915  fsumss  15254  fsumless  15323  cvgcmpce  15345  fprodss  15473  rpnnen2lem9  15746  isstruct2  16676  structcnvcnv  16680  fsets  16698  strleun  16775  strle1  16776  mreexexlem2d  17102  gsumpropd2lem  18105  symgfixf1  18783  f1omvdmvd  18789  mvdco  18791  f1omvdconj  18792  pmtrfb  18811  pmtrfconj  18812  symggen  18816  symggen2  18817  psgnunilem1  18839  frgpnabllem2  19213  dprdss  19370  dprd2da  19383  dmdprdsplit2lem  19386  dpjidcl  19399  ablfac1b  19411  ablfac1eu  19414  isdrng2  19731  drngmcl  19734  drngid2  19737  isdrngd  19746  cntzsdrg  19800  subdrgint  19801  xrs1mnd  20355  xrs10  20356  xrs1cmn  20357  xrge0subm  20358  xrge0cmn  20359  cnmgpid  20379  cnmsubglem  20380  expghm  20416  dsmmfi  20654  islinds2  20729  lindsind2  20735  lindfrn  20737  islindf4  20754  mdetdiaglem  21449  mdetrsca2  21455  mdetrlin2  21458  mdetralt  21459  mdetunilem5  21467  mdetunilem9  21471  maducoeval2  21491  smadiadetglem1  21522  isopn2  21883  ntrval2  21902  ntrdif  21903  clsdif  21904  ntrss  21906  cmclsopn  21913  discld  21940  mretopd  21943  lpsscls  21992  restntr  22033  cmpcld  22253  2ndcsep  22310  1stccnp  22313  llycmpkgen2  22401  1stckgen  22405  txkgen  22503  qtopcld  22564  qtopcmap  22570  kqdisj  22583  isufil2  22759  ufileu  22770  filufint  22771  fixufil  22773  cfinufil  22779  ufilen  22781  fin1aufil  22783  supnfcls  22871  flimfnfcls  22879  alexsublem  22895  alexsubALTlem3  22900  cldsubg  22962  imasdsf1olem  23225  recld2  23665  sszcld  23668  xrge0gsumle  23684  divcn  23719  cdivcncf  23772  bcth3  24182  ismbl2  24378  cmmbl  24385  nulmbl  24386  nulmbl2  24387  unmbl  24388  voliunlem1  24401  voliunlem2  24402  ioombl1lem4  24412  ioombl1  24413  uniioombllem3  24436  mbfss  24497  itg1cl  24536  itg1ge0  24537  i1f0  24538  i1f1  24541  i1fmul  24547  itg1addlem4  24550  itg1addlem4OLD  24551  itg1mulc  24556  itg10a  24562  itg1ge0a  24563  itg1climres  24566  itg2cnlem1  24613  itgioo  24667  itgsplitioo  24689  limcdif  24727  ellimc2  24728  ellimc3  24730  limcflflem  24731  limcflf  24732  limcmo  24733  limcresi  24736  dvreslem  24760  dvres2lem  24761  dvidlem  24766  dvcnp2  24771  dvaddbr  24789  dvmulbr  24790  dvcobr  24797  dvrec  24806  dvcnvlem  24827  lhop1lem  24864  lhop  24867  tdeglem4  24911  tdeglem4OLD  24912  deg1n0ima  24941  aacjcl  25174  taylthlem2  25220  abelth  25287  logcnlem5  25488  dvlog2  25495  efopnlem2  25499  dvcncxp1  25583  dvcnsqrt  25584  cxpcn2  25586  sqrtcn  25590  efrlim  25806  jensen  25825  amgm  25827  lgamgulmlem2  25866  lgamucov  25874  wilthlem2  25905  dchrelbas2  26072  rpvmasum2  26347  dchrisum0re  26348  dchrisum0lem3  26354  dchrisum0  26355  tgisline  26672  upgrss  27133  frgrwopreg2  28356  difxp1ss  30543  difxp2ss  30544  xrge00  30968  symgcom2  31026  pmtrcnel  31031  pmtrcnel2  31032  pmtrcnelor  31033  cycpmrn  31083  tocyccntz  31084  submatres  31424  madjusmdetlem2  31446  madjusmdetlem3  31447  qtophaus  31454  fsumcvg4  31568  gsumesum  31693  pwsiga  31764  sigainb  31770  carsggect  31951  omsmeas  31956  sitgclg  31975  ballotlemfelz  32123  ballotlemfp1  32124  ballotth  32170  cxpcncf1  32241  logdivsqrle  32296  hgt750lemb  32302  kur14lem6  32840  kur14lem7  32841  cvmscld  32902  satfvsucsuc  32994  satfrnmapom  32999  mclsppslem  33212  fundmpss  33410  frind  33460  frr1  33507  relsset  33876  limitssson  33899  fnsingle  33907  funimage  33916  cldbnd  34201  clsun  34203  topdifinffinlem  35204  inunissunidif  35232  pibt2  35274  matunitlindflem1  35459  poimirlem8  35471  poimirlem26  35489  poimirlem30  35493  mblfinlem3  35502  mblfinlem4  35503  ismblfin  35504  voliunnfl  35507  cnambfre  35511  dvtan  35513  dvasin  35547  dvacos  35548  areacirclem4  35554  fdc  35589  divrngcl  35801  isdrngo2  35802  isdrngo3  35803  islsati  36694  hdmap14lem2a  39567  prjspreln0  40097  prjspvs  40098  prjspeclsp  40100  0prjspnrel  40113  istopclsd  40166  diophin  40238  dnnumch1  40513  isdomn3  40673  deg1mhm  40676  gneispace  41362  inaex  41529  sumnnodd  42789  cncficcgt0  43047  cncfiooicclem1  43052  cxpcncf2  43058  dirkercncflem2  43263  fourierdlem62  43327  fourierdlem66  43331  fourierdlem68  43333  fourierdlem95  43360  etransclem24  43417  etransclem44  43437  gsumge0cl  43527  sge0fodjrnlem  43572  carageniuncllem1  43677  smfresal  43937  lindslinindimp2lem2  45416  iscnrm3rlem2  45851  amgmlemALT  46121