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

Theorem difss 3278
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 3273 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3159 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3124    C_ wss 3127
This theorem is referenced by:  difssd  3279  difss2  3280  ssdifss  3282  disj4  3478  0dif  3500  uneqdifeq  3517  difsnpss  3732  unidif  3833  iunxdif2  3924  difexg  4136  tz7.7  4390  tfi  4616  peano5  4651  reldif  4793  cnvdif  5075  fresaun  5350  fresaunres2  5351  resdif  5432  fndmdif  5563  difxp  6087  oev  6481  oacomf1olem  6530  oelim2  6561  swoer  6656  swoord1  6657  swoord2  6658  boxcutc  6827  undom  6918  domunsncan  6930  sbthlem1  6939  sbthlem2  6940  sbthlem4  6942  sbthlem5  6943  limenpsi  7004  phplem2  7009  php  7013  php3  7015  pssnn  7049  diffi  7057  frfi  7070  fofinf1o  7105  ixpfi2  7122  elfiun  7151  marypha1lem  7154  wemapso  7234  inf3lem3  7299  infdifsn  7325  cantnflem2  7360  dfac8alem  7624  numacn  7644  acnnum  7647  acndom2  7649  inffien  7658  kmlem5  7748  infdif  7803  infdif2  7804  ackbij1lem12  7825  ackbij1lem18  7831  fictb  7839  ssfin4  7904  fin23lem7  7910  fin23lem11  7911  fin23lem26  7919  fin23lem28  7934  fin23lem29  7935  fin23lem30  7936  isf32lem8  7954  compsscnvlem  7964  isf34lem2  7967  compssiso  7968  isf34lem4  7971  enfin1ai  7978  fin1a2lem7  8000  domtriomlem  8036  axcclem  8051  zornn0g  8100  ttukey2g  8111  konigthlem  8158  fpwwe2  8233  wundif  8304  pinn  8470  niex  8473  ltsopi  8480  dmaddpi  8482  dmmulpi  8483  lerelxr  8856  mulnzcnopr  9382  dflt2  10450  expcl2lem  11082  expclzlem  11094  hashun2  11332  fsumss  12164  fsumless  12220  cvgcmpce  12242  rpnnen2lem9  12464  rpnnen2lem11  12466  ramub1lem1  13036  ramub1lem2  13037  isstruct2  13120  structcnvcnv  13122  strleun  13201  strle1  13202  mreexexlem2d  13510  frgpnabllem2  15125  dprdfeq0  15220  dprdss  15227  dprd2da  15240  dmdprdsplit2lem  15243  dpjf  15255  dpjidcl  15256  dpjlid  15259  dpjghm  15261  ablfac1b  15268  ablfac1eulem  15270  ablfac1eu  15271  isdrng2  15485  drngmcl  15488  drngid2  15491  isdrngd  15500  lbspss  15798  lspsolv  15859  lsppratlem1  15863  lsppratlem2  15864  lsppratlem3  15865  lsppratlem4  15866  lspprat  15869  islbs2  15870  islbs3  15871  lbsextlem2  15875  lbsextlem3  15876  lbsextlem4  15877  xrs1mnd  16372  xrs10  16373  xrs1cmn  16374  xrge0subm  16375  xrge0cmn  16376  cnmsubglem  16397  expghm  16413  isopn2  16732  clsval2  16750  ntrval2  16751  ntrdif  16752  clsdif  16753  ntrss  16755  cmclsopn  16762  cmntrcld  16763  discld  16789  mretopd  16792  lpsscls  16836  lpss3  16839  restntr  16875  restlp  16876  lpcls  17055  cmpcld  17092  hauscmplem  17096  2ndcsep  17148  1stccnp  17151  hausllycmp  17183  llycmpkgen2  17208  1stckgen  17212  txkgen  17309  qtopcld  17367  qtoprest  17371  qtopcmap  17373  kqdisj  17386  trfil3  17546  isufil2  17566  ufileu  17577  filufint  17578  fixufil  17580  cfinufil  17586  ufinffr  17587  ufilen  17588  fin1aufil  17590  supnfcls  17678  fclscf  17683  flimfnfcls  17686  alexsublem  17701  alexsubALTlem3  17706  cldsubg  17756  imasdsf1olem  17900  blcld  18014  recld2  18283  xrge0gsumle  18301  divcn  18335  cdivcncf  18383  evth  18420  lebnumlem1  18422  lebnumlem2  18423  lebnumlem3  18424  bcthlem2  18710  bcthlem3  18711  bcthlem5  18713  bcth3  18716  ismbl2  18849  cmmbl  18855  nulmbl  18856  nulmbl2  18857  unmbl  18858  shftmbl  18859  volinun  18866  iundisj2  18869  voliunlem1  18870  voliunlem2  18871  volsup  18876  ioombl1lem4  18881  ioombl1  18882  uniiccdif  18896  uniioombllem3  18903  uniioombllem5  18905  uniioombl  18907  uniiccmbl  18908  mbfss  18964  itg1val2  19002  itg1cl  19003  itg1ge0  19004  i1f0  19005  i1f1  19008  i1fadd  19013  i1fmul  19014  itg1addlem4  19017  itg1addlem5  19018  i1fmulc  19021  itg1mulc  19022  itg10a  19028  itg1ge0a  19029  itg1climres  19032  mbfi1fseqlem4  19036  itg2cnlem1  19079  itg2cnlem2  19080  itgss3  19132  itgioo  19133  itgsplitioo  19155  limcdif  19189  ellimc2  19190  limcnlp  19191  ellimc3  19192  limcflflem  19193  limcflf  19194  limcmo  19195  limcmpt2  19197  limcresi  19198  perfdvf  19216  dvreslem  19222  dvres2lem  19223  dvidlem  19228  dvcnp2  19232  dvaddbr  19250  dvmulbr  19251  dvcobr  19258  dvrec  19267  dvcnvlem  19286  dvexp3  19288  dveflem  19289  dvferm1  19295  dvferm2  19297  lhop1lem  19323  lhop  19326  dvcnvrelem2  19328  ftc1lem6  19351  tdeglem4  19409  deg1n0ima  19438  ig1peu  19520  ig1pdvds  19525  aacjcl  19670  taylthlem1  19715  taylthlem2  19716  ulmdvlem3  19742  abelth  19780  logcnlem5  19956  dvlog2  19963  efopnlem2  19967  cxpcn2  20049  sqrcn  20053  rlimcnp  20223  efrlim  20227  jensen  20246  amgm  20248  wilthlem2  20270  dchrelbas2  20439  chebbnd1lem1  20581  rpvmasum2  20624  dchrisum0re  20625  dchrisum0lem3  20631  dchrisum0  20632  ballotlemfelz  23011  ballotlemfp1  23012  ballotth  23058  kur14lem6  23115  kur14lem7  23116  cvmscld  23177  umgrass  23244  umgraex  23248  fundmpss  23492  wfi  23577  frind  23613  wfrlem16  23641  relsset  23805  fnsingle  23834  funimage  23843  prl  24535  islp3  24882  islimrs4  24950  cldbnd  25612  clsun  25614  neibastop2lem  25677  fdc  25823  divrngcl  25956  isdrngo2  25957  isdrngo3  25958  ralxpmap  26129  istopclsd  26143  eldioph2lem2  26208  diophin  26220  setindtr  26485  dnnumch1  26509  dsmmfi  26572  frlmsslss2  26613  frlmlbs  26617  islinds2  26651  lindsind2  26657  lindfrn  26659  islindf4  26676  f1omvdmvd  26754  mvdco  26756  f1omvdconj  26757  pmtrfinv  26770  pmtrfb  26774  pmtrfconj  26775  symggen  26779  symggen2  26780  psgnunilem1  26784  cnmsgngrp  26804  psgnghm2  26806  cntzsdrg  26878  isdomn3  26891  deg1mhm  26894  stoweidlem28  27146  stoweidlem50  27168  stoweidlem57  27175  islsati  28434  lsatfixedN  28449  dochsnkr  30912  hdmaprnlem4tN  31295  hdmap14lem2a  31310
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator