Theorem difss 4090

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

Syntax hints:   ∖ cdif 3900   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920

This theorem is referenced by:  difssd  4091  difss2  4092  ssdifss  4094  0dif  4359  disj4  4413  difsnpss  4765  unidif  4900  iunxdif2  5011  difexg  5276  difelpw  5301  reldif  5772  cnvdif  6109  difxp  6130  frpoind  6308  tz7.7  6351  fresaun  6713  fresaunres2  6714  resdif  6803  fndmdif  6996  tfi  7805  peano5  7845  oelim2  8533  swoer  8677  swoord1  8678  swoord2  8679  ralxpmap  8846  boxcutc  8891  undom  9005  domunsncan  9017  sbthlem2  9028  sbthlem4  9030  sbthlem5  9031  limenpsi  9092  diffi  9111  php3  9145  frfi  9197  fofinf1o  9244  ixpfi2  9262  elfiun  9345  marypha1lem  9348  wemapso  9468  infdifsn  9578  cantnflem2  9611  frind  9674  frr1  9683  dfac8alem  9951  acnnum  9974  inffien  9985  kmlem5  10077  infdif  10130  infdif2  10131  ackbij1lem18  10158  fictb  10166  fin23lem7  10238  fin23lem11  10239  fin23lem28  10262  fin23lem30  10264  compsscnvlem  10292  isf34lem2  10295  compssiso  10296  isf34lem4  10299  fin1a2lem7  10328  axcclem  10379  zornn0g  10427  ttukey2g  10438  pinn  10801  niex  10804  ltsopi  10811  dmaddpi  10813  dmmulpi  10814  lerelxr  11207  mulnzcnf  11795  dflt2  13074  expcl2lem  14008  expclzlem  14018  hashun2  14318  fsumss  15660  fsumless  15731  cvgcmpce  15753  fprodss  15883  rpnnen2lem9  16159  isstruct2  17088  structcnvcnv  17092  strleun  17096  strle1  17097  fsets  17108  mreexexlem2d  17580  gsumpropd2lem  18616  symgfixf1  19378  f1omvdmvd  19384  mvdco  19386  f1omvdconj  19387  pmtrfb  19406  pmtrfconj  19407  symggen  19411  symggen2  19412  psgnunilem1  19434  frgpnabllem2  19815  dprdss  19972  dprd2da  19985  dmdprdsplit2lem  19988  dpjidcl  20001  ablfac1b  20013  ablfac1eu  20016  isdomn3  20660  isdrng2  20688  drngmclOLD  20696  drngid2  20697  isdrngd  20710  isdrngdOLD  20712  cntzsdrg  20747  subdrgint  20748  cnmgpid  21396  cnmsubglem  21397  xrs1mnd  21407  xrs10  21408  xrs1cmn  21409  xrge0subm  21410  xrge0cmn  21411  expghm  21442  dsmmfi  21705  islinds2  21780  lindsind2  21786  lindfrn  21788  islindf4  21805  psdmul  22121  mdetdiaglem  22554  mdetrsca2  22560  mdetrlin2  22563  mdetralt  22564  mdetunilem5  22572  mdetunilem9  22576  maducoeval2  22596  smadiadetglem1  22627  isopn2  22988  ntrval2  23007  ntrdif  23008  clsdif  23009  ntrss  23011  cmclsopn  23018  discld  23045  mretopd  23048  lpsscls  23097  restntr  23138  cmpcld  23358  2ndcsep  23415  1stccnp  23418  llycmpkgen2  23506  1stckgen  23510  txkgen  23608  qtopcld  23669  qtopcmap  23675  kqdisj  23688  isufil2  23864  ufileu  23875  filufint  23876  fixufil  23878  cfinufil  23884  ufilen  23886  fin1aufil  23888  supnfcls  23976  flimfnfcls  23984  alexsublem  24000  alexsubALTlem3  24005  cldsubg  24067  imasdsf1olem  24329  recld2  24771  sszcld  24774  xrge0gsumle  24790  divcnOLD  24825  divcn  24827  cdivcncf  24882  bcth3  25299  ismbl2  25496  cmmbl  25503  nulmbl  25504  nulmbl2  25505  unmbl  25506  voliunlem1  25519  voliunlem2  25520  ioombl1lem4  25530  ioombl1  25531  uniioombllem3  25554  mbfss  25615  itg1cl  25654  itg1ge0  25655  i1f0  25656  i1f1  25659  i1fmul  25665  itg1addlem4  25668  itg1mulc  25673  itg10a  25679  itg1ge0a  25680  itg1climres  25683  itg2cnlem1  25730  itgioo  25785  itgsplitioo  25807  limcdif  25845  ellimc2  25846  ellimc3  25848  limcflflem  25849  limcflf  25850  limcmo  25851  limcresi  25854  dvreslem  25878  dvres2lem  25879  dvidlem  25884  dvcnp2  25889  dvcnp2OLD  25890  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcobr  25917  dvcobrOLD  25918  dvrec  25927  dvcnvlem  25948  lhop1lem  25986  lhop  25989  tdeglem4  26033  deg1n0ima  26062  aacjcl  26303  taylthlem2  26350  taylthlem2OLD  26351  abelth  26419  logcnlem5  26623  dvlog2  26630  efopnlem2  26634  dvcncxp1  26720  dvcnsqrt  26721  cxpcn2  26724  sqrtcn  26728  efrlim  26947  efrlimOLD  26948  jensen  26967  amgm  26969  lgamgulmlem2  27008  lgamucov  27016  wilthlem2  27047  dchrelbas2  27216  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem3  27498  dchrisum0  27499  nnssn0s  28329  tgisline  28711  upgrss  29173  frgrwopreg2  30406  difxp1ss  32608  difxp2ss  32609  xrge00  33106  symgcom2  33177  pmtrcnel  33182  pmtrcnel2  33183  pmtrcnelor  33184  cycpmrn  33236  tocyccntz  33237  evlextv  33718  vietalem  33755  submatres  33983  madjusmdetlem2  34005  madjusmdetlem3  34006  qtophaus  34013  fsumcvg4  34127  gsumesum  34236  pwsiga  34307  sigainb  34313  carsggect  34495  omsmeas  34500  sitgclg  34519  ballotlemfelz  34668  ballotlemfp1  34669  ballotth  34715  cxpcncf1  34772  logdivsqrle  34827  hgt750lemb  34833  fineqvnttrclse  35299  kur14lem6  35424  kur14lem7  35425  cvmscld  35486  satfvsucsuc  35578  satfrnmapom  35583  mclsppslem  35796  fundmpss  35980  relsset  36099  limitssson  36122  fnsingle  36130  funimage  36139  cldbnd  36539  clsun  36541  topdifinffinlem  37599  inunissunidif  37627  pibt2  37669  matunitlindflem1  37864  poimirlem8  37876  poimirlem26  37894  poimirlem30  37898  mblfinlem3  37907  mblfinlem4  37908  ismblfin  37909  voliunnfl  37912  cnambfre  37916  dvtan  37918  dvasin  37952  dvacos  37953  areacirclem4  37959  fdc  37993  divrngcl  38205  isdrngo2  38206  isdrngo3  38207  islsati  39367  hdmap14lem2a  42240  redvmptabs  42727  prjspreln0  42964  prjspvs  42965  prjspeclsp  42967  0prjspnrel  42982  istopclsd  43054  diophin  43126  dnnumch1  43398  deg1mhm  43554  gneispace  44487  inaex  44650  sumnnodd  45987  cncficcgt0  46243  cncfiooicclem1  46248  cxpcncf2  46254  dirkercncflem2  46459  fourierdlem62  46523  fourierdlem66  46527  fourierdlem68  46529  fourierdlem95  46556  etransclem24  46613  etransclem44  46633  gsumge0cl  46726  sge0fodjrnlem  46771  carageniuncllem1  46876  smfresal  47143  dfnbgrss  48209  dfnbgrss2  48216  lindslinindimp2lem2  48816  iscnrm3rlem2  49297  amgmlemALT  50159