Theorem difss 3888

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

Syntax hints:   ∖ cdif 3720   ⊆ wss 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737

This theorem is referenced by:  difssd  3889  difss2  3890  ssdifss  3892  0dif  4121  disj4  4169  difsnpss  4473  unidif  4607  iunxdif2  4702  difexg  4942  reldif  5377  cnvdif  5680  difxp  5699  wfi  5856  tz7.7  5892  fresaun  6215  fresaunres2  6216  resdif  6298  fndmdif  6464  tfi  7200  peano5  7236  wfrlem16  7583  oev  7748  oelim2  7829  swoer  7926  swoord1  7927  swoord2  7928  ralxpmap  8061  boxcutc  8105  undom  8204  domunsncan  8216  sbthlem2  8227  sbthlem4  8229  sbthlem5  8230  limenpsi  8291  phplem2  8296  php  8300  php3  8302  pssnn  8334  diffi  8348  frfi  8361  fofinf1o  8397  ixpfi2  8420  elfiun  8492  marypha1lem  8495  wemapso  8612  infdifsn  8718  cantnflem2  8751  dfac8alem  9052  acnnum  9075  inffien  9086  kmlem5  9178  infdif  9233  infdif2  9234  ackbij1lem18  9261  fictb  9269  fin23lem7  9340  fin23lem11  9341  fin23lem28  9364  fin23lem30  9366  compsscnvlem  9394  isf34lem2  9397  compssiso  9398  isf34lem4  9401  fin1a2lem7  9430  domtriomlem  9466  axcclem  9481  zornn0g  9529  ttukey2g  9540  konigthlem  9592  pinn  9902  niex  9905  ltsopi  9912  dmaddpi  9914  dmmulpi  9915  lerelxr  10303  mulnzcnopr  10875  dflt2  12186  expcl2lem  13079  expclzlem  13091  hashun2  13374  fsumss  14664  fsumless  14735  cvgcmpce  14757  fprodss  14885  rpnnen2lem9  15157  isstruct2  16074  structcnvcnv  16078  fsets  16098  strleun  16180  strle1  16181  mreexexlem2d  16513  gsumpropd2lem  17481  symgfixf1  18064  f1omvdmvd  18070  mvdco  18072  f1omvdconj  18073  pmtrfb  18092  pmtrfconj  18093  symggen  18097  symggen2  18098  psgnunilem1  18120  frgpnabllem2  18484  dprdss  18636  dprd2da  18649  dmdprdsplit2lem  18652  dpjidcl  18665  ablfac1b  18677  ablfac1eu  18680  isdrng2  18967  drngmcl  18970  drngid2  18973  isdrngd  18982  xrs1mnd  19999  xrs10  20000  xrs1cmn  20001  xrge0subm  20002  xrge0cmn  20003  cnmgpid  20023  cnmsubglem  20024  expghm  20059  cnmsgngrp  20140  psgninv  20143  dsmmfi  20299  islinds2  20369  lindsind2  20375  lindfrn  20377  islindf4  20394  mdetdiaglem  20622  mdetrsca2  20628  mdetrlin2  20631  mdetralt  20632  mdetunilem5  20640  mdetunilem9  20644  maducoeval2  20664  smadiadetglem1  20696  isopn2  21057  ntrval2  21076  ntrdif  21077  clsdif  21078  ntrss  21080  cmclsopn  21087  discld  21114  mretopd  21117  lpsscls  21166  restntr  21207  cmpcld  21426  2ndcsep  21483  1stccnp  21486  llycmpkgen2  21574  1stckgen  21578  txkgen  21676  qtopcld  21737  qtopcmap  21743  kqdisj  21756  isufil2  21932  ufileu  21943  filufint  21944  fixufil  21946  cfinufil  21952  ufilen  21954  fin1aufil  21956  supnfcls  22044  flimfnfcls  22052  alexsublem  22068  alexsubALTlem3  22073  cldsubg  22134  imasdsf1olem  22398  recld2  22837  sszcld  22840  xrge0gsumle  22856  divcn  22891  cdivcncf  22940  bcth3  23347  ismbl2  23515  cmmbl  23522  nulmbl  23523  nulmbl2  23524  unmbl  23525  voliunlem1  23538  voliunlem2  23539  ioombl1lem4  23549  ioombl1  23550  uniioombllem3  23573  mbfss  23633  itg1cl  23672  itg1ge0  23673  i1f0  23674  i1f1  23677  i1fmul  23683  itg1addlem4  23686  itg1mulc  23691  itg10a  23697  itg1ge0a  23698  itg1climres  23701  itg2cnlem1  23748  itgioo  23802  itgsplitioo  23824  limcdif  23860  ellimc2  23861  ellimc3  23863  limcflflem  23864  limcflf  23865  limcmo  23866  limcresi  23869  dvreslem  23893  dvres2lem  23894  dvidlem  23899  dvcnp2  23903  dvaddbr  23921  dvmulbr  23922  dvcobr  23929  dvrec  23938  dvcnvlem  23959  lhop1lem  23996  lhop  23999  tdeglem4  24040  deg1n0ima  24069  aacjcl  24302  taylthlem2  24348  abelth  24415  logcnlem5  24613  dvlog2  24620  efopnlem2  24624  dvcncxp1  24705  dvcnsqrt  24706  cxpcn2  24708  sqrtcn  24712  efrlim  24917  jensen  24936  amgm  24938  lgamgulmlem2  24977  lgamucov  24985  wilthlem2  25016  dchrelbas2  25183  rpvmasum2  25422  dchrisum0re  25423  dchrisum0lem3  25429  dchrisum0  25430  tgisline  25743  upgrss  26204  frgrwopreg2  27501  xrge00  30026  submatres  30212  madjusmdetlem2  30234  madjusmdetlem3  30235  qtophaus  30243  fsumcvg4  30336  gsumesum  30461  pwsiga  30533  sigainb  30539  carsggect  30720  omsmeas  30725  sitgclg  30744  ballotlemfelz  30892  ballotlemfp1  30893  ballotth  30939  cxpcncf1  31013  logdivsqrle  31068  hgt750lemb  31074  kur14lem6  31531  kur14lem7  31532  cvmscld  31593  mclsppslem  31818  fundmpss  32002  frpoind  32077  frind  32080  relsset  32332  limitssson  32355  fnsingle  32363  funimage  32372  cldbnd  32658  clsun  32660  topdifinffinlem  33532  matunitlindflem1  33738  poimirlem8  33750  poimirlem26  33768  poimirlem30  33772  mblfinlem3  33781  mblfinlem4  33782  ismblfin  33783  voliunnfl  33786  cnambfre  33790  dvtan  33792  dvasin  33828  dvacos  33829  areacirclem4  33835  fdc  33873  divrngcl  34088  isdrngo2  34089  isdrngo3  34090  islsati  34803  hdmap14lem2a  37677  istopclsd  37789  diophin  37862  dnnumch1  38140  cntzsdrg  38298  isdomn3  38308  deg1mhm  38311  gneispace  38958  sumnnodd  40380  cncficcgt0  40619  cncfiooicclem1  40624  cxpcncf2  40631  dirkercncflem2  40838  fourierdlem62  40902  fourierdlem66  40906  fourierdlem68  40908  fourierdlem95  40935  etransclem24  40992  etransclem44  41012  gsumge0cl  41105  sge0fodjrnlem  41150  carageniuncllem1  41255  smfresal  41515  lindslinindimp2lem2  42776  amgmlemALT  43080