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

Theorem difss 3304
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eldifi 3299 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3185 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3150    C_ wss 3153
This theorem is referenced by:  difssd  3305  difss2  3306  ssdifss  3308  disj4  3504  0dif  3526  uneqdifeq  3543  difsnpss  3759  unidif  3860  iunxdif2  3951  difexg  4163  tz7.7  4417  tfi  4643  peano5  4678  reldif  4804  cnvdif  5086  fresaun  5378  fresaunres2  5379  resdif  5460  fndmdif  5591  difxp  6115  oev  6509  oacomf1olem  6558  oelim2  6589  swoer  6684  swoord1  6685  swoord2  6686  boxcutc  6855  undom  6946  domunsncan  6958  sbthlem1  6967  sbthlem2  6968  sbthlem4  6970  sbthlem5  6971  limenpsi  7032  phplem2  7037  php  7041  php3  7043  pssnn  7077  diffi  7085  frfi  7098  fofinf1o  7133  ixpfi2  7150  elfiun  7179  marypha1lem  7182  wemapso  7262  inf3lem3  7327  infdifsn  7353  cantnflem2  7388  dfac8alem  7652  numacn  7672  acnnum  7675  acndom2  7677  inffien  7686  kmlem5  7776  infdif  7831  infdif2  7832  ackbij1lem12  7853  ackbij1lem18  7859  fictb  7867  ssfin4  7932  fin23lem7  7938  fin23lem11  7939  fin23lem26  7947  fin23lem28  7962  fin23lem29  7963  fin23lem30  7964  isf32lem8  7982  compsscnvlem  7992  isf34lem2  7995  compssiso  7996  isf34lem4  7999  enfin1ai  8006  fin1a2lem7  8028  domtriomlem  8064  axcclem  8079  zornn0g  8128  ttukey2g  8139  konigthlem  8186  fpwwe2  8261  wundif  8332  pinn  8498  niex  8501  ltsopi  8508  dmaddpi  8510  dmmulpi  8511  lerelxr  8884  mulnzcnopr  9410  dflt2  10478  expcl2lem  11111  expclzlem  11123  hashun2  11361  fsumss  12194  fsumless  12250  cvgcmpce  12272  rpnnen2lem9  12497  rpnnen2lem11  12499  ramub1lem1  13069  ramub1lem2  13070  isstruct2  13153  structcnvcnv  13155  strleun  13234  strle1  13235  mreexexlem2d  13543  frgpnabllem2  15158  dprdfeq0  15253  dprdss  15260  dprd2da  15273  dmdprdsplit2lem  15276  dpjf  15288  dpjidcl  15289  dpjlid  15292  dpjghm  15294  ablfac1b  15301  ablfac1eulem  15303  ablfac1eu  15304  isdrng2  15518  drngmcl  15521  drngid2  15524  isdrngd  15533  lbspss  15831  lspsolv  15892  lsppratlem1  15896  lsppratlem2  15897  lsppratlem3  15898  lsppratlem4  15899  lspprat  15902  islbs2  15903  islbs3  15904  lbsextlem2  15908  lbsextlem3  15909  lbsextlem4  15910  xrs1mnd  16405  xrs10  16406  xrs1cmn  16407  xrge0subm  16408  xrge0cmn  16409  cnmsubglem  16430  expghm  16446  isopn2  16765  clsval2  16783  ntrval2  16784  ntrdif  16785  clsdif  16786  ntrss  16788  cmclsopn  16795  cmntrcld  16796  discld  16822  mretopd  16825  lpsscls  16869  lpss3  16872  restntr  16908  restlp  16909  lpcls  17088  cmpcld  17125  hauscmplem  17129  2ndcsep  17181  1stccnp  17184  hausllycmp  17216  llycmpkgen2  17241  1stckgen  17245  txkgen  17342  qtopcld  17400  qtoprest  17404  qtopcmap  17406  kqdisj  17419  trfil3  17579  isufil2  17599  ufileu  17610  filufint  17611  fixufil  17613  cfinufil  17619  ufinffr  17620  ufilen  17621  fin1aufil  17623  supnfcls  17711  fclscf  17716  flimfnfcls  17719  alexsublem  17734  alexsubALTlem3  17739  cldsubg  17789  imasdsf1olem  17933  blcld  18047  recld2  18316  xrge0gsumle  18334  divcn  18368  cdivcncf  18416  evth  18453  lebnumlem1  18455  lebnumlem2  18456  lebnumlem3  18457  bcthlem2  18743  bcthlem3  18744  bcthlem5  18746  bcth3  18749  ismbl2  18882  cmmbl  18888  nulmbl  18889  nulmbl2  18890  unmbl  18891  shftmbl  18892  volinun  18899  iundisj2  18902  voliunlem1  18903  voliunlem2  18904  volsup  18909  ioombl1lem4  18914  ioombl1  18915  uniiccdif  18929  uniioombllem3  18936  uniioombllem5  18938  uniioombl  18940  uniiccmbl  18941  mbfss  18997  itg1val2  19035  itg1cl  19036  itg1ge0  19037  i1f0  19038  i1f1  19041  i1fadd  19046  i1fmul  19047  itg1addlem4  19050  itg1addlem5  19051  i1fmulc  19054  itg1mulc  19055  itg10a  19061  itg1ge0a  19062  itg1climres  19065  mbfi1fseqlem4  19069  itg2cnlem1  19112  itg2cnlem2  19113  itgss3  19165  itgioo  19166  itgsplitioo  19188  limcdif  19222  ellimc2  19223  limcnlp  19224  ellimc3  19225  limcflflem  19226  limcflf  19227  limcmo  19228  limcmpt2  19230  limcresi  19231  perfdvf  19249  dvreslem  19255  dvres2lem  19256  dvidlem  19261  dvcnp2  19265  dvaddbr  19283  dvmulbr  19284  dvcobr  19291  dvrec  19300  dvcnvlem  19319  dvexp3  19321  dveflem  19322  dvferm1  19328  dvferm2  19330  lhop1lem  19356  lhop  19359  dvcnvrelem2  19361  ftc1lem6  19384  tdeglem4  19442  deg1n0ima  19471  ig1peu  19553  ig1pdvds  19558  aacjcl  19703  taylthlem1  19748  taylthlem2  19749  ulmdvlem3  19775  abelth  19813  logcnlem5  19989  dvlog2  19996  efopnlem2  20000  cxpcn2  20082  sqrcn  20086  rlimcnp  20256  efrlim  20260  jensen  20279  amgm  20281  wilthlem2  20303  dchrelbas2  20472  chebbnd1lem1  20614  rpvmasum2  20657  dchrisum0re  20658  dchrisum0lem3  20664  dchrisum0  20665  ballotlemfelz  23045  ballotlemfp1  23046  ballotth  23092  kur14lem6  23149  kur14lem7  23150  cvmscld  23211  umgrass  23278  umgraex  23282  fundmpss  23526  wfi  23611  frind  23647  wfrlem16  23675  relsset  23839  fnsingle  23868  funimage  23877  areacirclem5  24339  prl  24578  islp3  24925  islimrs4  24993  cldbnd  25655  clsun  25657  neibastop2lem  25720  fdc  25866  divrngcl  25999  isdrngo2  26000  isdrngo3  26001  ralxpmap  26172  istopclsd  26186  eldioph2lem2  26251  diophin  26263  setindtr  26528  dnnumch1  26552  dsmmfi  26615  frlmsslss2  26656  frlmlbs  26660  islinds2  26694  lindsind2  26700  lindfrn  26702  islindf4  26719  f1omvdmvd  26797  mvdco  26799  f1omvdconj  26800  pmtrfinv  26813  pmtrfb  26817  pmtrfconj  26818  symggen  26822  symggen2  26823  psgnunilem1  26827  cnmsgngrp  26847  psgnghm2  26849  cntzsdrg  26921  isdomn3  26934  deg1mhm  26937  stoweidlem28  27188  stoweidlem50  27210  stoweidlem57  27217  islsati  28463  lsatfixedN  28478  dochsnkr  30941  hdmaprnlem4tN  31324  hdmap14lem2a  31339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator