MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difss Unicode version

Theorem difss 3245
Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
difss  |-  ( A 
\  B )  C_  A

Proof of Theorem difss
StepHypRef Expression
1 eldifi 3240 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3126 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3091    C_ wss 3094
This theorem is referenced by:  difssd  3246  difss2  3247  ssdifss  3249  disj4  3445  0dif  3467  uneqdifeq  3484  difsnpss  3699  unidif  3800  iunxdif2  3891  difexg  4102  tz7.7  4355  tfi  4581  peano5  4616  reldif  4758  cnvdif  5040  fresaun  5315  fresaunres2  5316  resdif  5397  fndmdif  5528  difxp  6052  oev  6446  oacomf1olem  6495  oelim2  6526  swoer  6621  swoord1  6622  swoord2  6623  boxcutc  6792  undom  6883  domunsncan  6895  sbthlem1  6904  sbthlem2  6905  sbthlem4  6907  sbthlem5  6908  limenpsi  6969  phplem2  6974  php  6978  php3  6980  pssnn  7014  diffi  7022  frfi  7035  fofinf1o  7070  ixpfi2  7087  elfiun  7116  marypha1lem  7119  wemapso  7199  inf3lem3  7264  infdifsn  7290  cantnflem2  7325  dfac8alem  7589  numacn  7609  acnnum  7612  acndom2  7614  inffien  7623  kmlem5  7713  infdif  7768  infdif2  7769  ackbij1lem12  7790  ackbij1lem18  7796  fictb  7804  ssfin4  7869  fin23lem7  7875  fin23lem11  7876  fin23lem26  7884  fin23lem28  7899  fin23lem29  7900  fin23lem30  7901  isf32lem8  7919  compsscnvlem  7929  isf34lem2  7932  compssiso  7933  isf34lem4  7936  enfin1ai  7943  fin1a2lem7  7965  domtriomlem  8001  axcclem  8016  zornn0g  8065  ttukey2g  8076  konigthlem  8123  fpwwe2  8198  wundif  8269  pinn  8435  niex  8438  ltsopi  8445  dmaddpi  8447  dmmulpi  8448  lerelxr  8821  mulnzcnopr  9347  dflt2  10414  expcl2lem  11046  expclzlem  11058  hashun2  11296  fsumss  12128  fsumless  12184  cvgcmpce  12206  rpnnen2lem9  12428  rpnnen2lem11  12430  ramub1lem1  13000  ramub1lem2  13001  isstruct2  13084  structcnvcnv  13086  strleun  13165  strle1  13166  mreexexlem2d  13474  frgpnabllem2  15089  dprdfeq0  15184  dprdss  15191  dprd2da  15204  dmdprdsplit2lem  15207  dpjf  15219  dpjidcl  15220  dpjlid  15223  dpjghm  15225  ablfac1b  15232  ablfac1eulem  15234  ablfac1eu  15235  isdrng2  15449  drngmcl  15452  drngid2  15455  isdrngd  15464  lbspss  15762  lspsolv  15823  lsppratlem1  15827  lsppratlem2  15828  lsppratlem3  15829  lsppratlem4  15830  lspprat  15833  islbs2  15834  islbs3  15835  lbsextlem2  15839  lbsextlem3  15840  lbsextlem4  15841  xrs1mnd  16336  xrs10  16337  xrs1cmn  16338  xrge0subm  16339  xrge0cmn  16340  cnmsubglem  16361  expghm  16377  isopn2  16696  clsval2  16714  ntrval2  16715  ntrdif  16716  clsdif  16717  ntrss  16719  cmclsopn  16726  cmntrcld  16727  discld  16753  mretopd  16756  lpsscls  16800  lpss3  16803  restntr  16839  restlp  16840  lpcls  17019  cmpcld  17056  hauscmplem  17060  2ndcsep  17112  1stccnp  17115  hausllycmp  17147  llycmpkgen2  17172  1stckgen  17176  txkgen  17273  qtopcld  17331  qtoprest  17335  qtopcmap  17337  kqdisj  17350  trfil3  17510  isufil2  17530  ufileu  17541  filufint  17542  fixufil  17544  cfinufil  17550  ufinffr  17551  ufilen  17552  fin1aufil  17554  supnfcls  17642  fclscf  17647  flimfnfcls  17650  alexsublem  17665  alexsubALTlem3  17670  cldsubg  17720  imasdsf1olem  17864  blcld  17978  recld2  18247  xrge0gsumle  18265  divcn  18299  cdivcncf  18347  evth  18384  lebnumlem1  18386  lebnumlem2  18387  lebnumlem3  18388  bcthlem2  18674  bcthlem3  18675  bcthlem5  18677  bcth3  18680  ismbl2  18813  cmmbl  18819  nulmbl  18820  nulmbl2  18821  unmbl  18822  shftmbl  18823  volinun  18830  iundisj2  18833  voliunlem1  18834  voliunlem2  18835  volsup  18840  ioombl1lem4  18845  ioombl1  18846  uniiccdif  18860  uniioombllem3  18867  uniioombllem5  18869  uniioombl  18871  uniiccmbl  18872  mbfss  18928  itg1val2  18966  itg1cl  18967  itg1ge0  18968  i1f0  18969  i1f1  18972  i1fadd  18977  i1fmul  18978  itg1addlem4  18981  itg1addlem5  18982  i1fmulc  18985  itg1mulc  18986  itg10a  18992  itg1ge0a  18993  itg1climres  18996  mbfi1fseqlem4  19000  itg2cnlem1  19043  itg2cnlem2  19044  itgss3  19096  itgioo  19097  itgsplitioo  19119  limcdif  19153  ellimc2  19154  limcnlp  19155  ellimc3  19156  limcflflem  19157  limcflf  19158  limcmo  19159  limcmpt2  19161  limcresi  19162  perfdvf  19180  dvreslem  19186  dvres2lem  19187  dvidlem  19192  dvcnp2  19196  dvaddbr  19214  dvmulbr  19215  dvcobr  19222  dvrec  19231  dvcnvlem  19250  dvexp3  19252  dveflem  19253  dvferm1  19259  dvferm2  19261  lhop1lem  19287  lhop  19290  dvcnvrelem2  19292  ftc1lem6  19315  tdeglem4  19373  deg1n0ima  19402  ig1peu  19484  ig1pdvds  19489  aacjcl  19634  taylthlem1  19679  taylthlem2  19680  ulmdvlem3  19706  abelth  19744  logcnlem5  19920  dvlog2  19927  efopnlem2  19931  cxpcn2  20013  sqrcn  20017  rlimcnp  20187  efrlim  20191  jensen  20210  amgm  20212  wilthlem2  20234  dchrelbas2  20403  chebbnd1lem1  20545  rpvmasum2  20588  dchrisum0re  20589  dchrisum0lem3  20595  dchrisum0  20596  ballotlemfelz  22975  ballotlemfp1  22976  ballotth  23022  kur14lem6  23079  kur14lem7  23080  cvmscld  23141  umgrass  23208  umgraex  23212  fundmpss  23456  wfi  23541  frind  23577  wfrlem16  23605  relsset  23769  fnsingle  23798  funimage  23807  prl  24499  islp3  24846  islimrs4  24914  cldbnd  25576  clsun  25578  neibastop2lem  25641  fdc  25787  divrngcl  25920  isdrngo2  25921  isdrngo3  25922  ralxpmap  26093  istopclsd  26107  eldioph2lem2  26172  diophin  26184  setindtr  26449  dnnumch1  26473  dsmmfi  26536  frlmsslss2  26577  frlmlbs  26581  islinds2  26615  lindsind2  26621  lindfrn  26623  islindf4  26640  f1omvdmvd  26718  mvdco  26720  f1omvdconj  26721  pmtrfinv  26734  pmtrfb  26738  pmtrfconj  26739  symggen  26743  symggen2  26744  psgnunilem1  26748  cnmsgngrp  26768  psgnghm2  26770  cntzsdrg  26842  isdomn3  26855  deg1mhm  26858  stoweidlem28  27077  stoweidlem50  27099  stoweidlem57  27106  islsati  28314  lsatfixedN  28329  dochsnkr  30792  hdmaprnlem4tN  31175  hdmap14lem2a  31190
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator