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

Theorem difss 3303
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 3298 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3184 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3149    C_ wss 3152
This theorem is referenced by:  difssd  3304  difss2  3305  ssdifss  3307  disj4  3503  0dif  3525  uneqdifeq  3542  difsnpss  3758  unidif  3859  iunxdif2  3950  difexg  4162  tz7.7  4418  tfi  4644  peano5  4679  reldif  4805  cnvdif  5087  fresaun  5412  fresaunres2  5413  resdif  5494  fndmdif  5629  difxp  6153  oev  6513  oacomf1olem  6562  oelim2  6593  swoer  6688  swoord1  6689  swoord2  6690  boxcutc  6859  undom  6950  domunsncan  6962  sbthlem1  6971  sbthlem2  6972  sbthlem4  6974  sbthlem5  6975  limenpsi  7036  phplem2  7041  php  7045  php3  7047  pssnn  7081  diffi  7089  frfi  7102  fofinf1o  7137  ixpfi2  7154  elfiun  7183  marypha1lem  7186  wemapso  7266  inf3lem3  7331  infdifsn  7357  cantnflem2  7392  dfac8alem  7656  numacn  7676  acnnum  7679  acndom2  7681  inffien  7690  kmlem5  7780  infdif  7835  infdif2  7836  ackbij1lem12  7857  ackbij1lem18  7863  fictb  7871  ssfin4  7936  fin23lem7  7942  fin23lem11  7943  fin23lem26  7951  fin23lem28  7966  fin23lem29  7967  fin23lem30  7968  isf32lem8  7986  compsscnvlem  7996  isf34lem2  7999  compssiso  8000  isf34lem4  8003  enfin1ai  8010  fin1a2lem7  8032  domtriomlem  8068  axcclem  8083  zornn0g  8132  ttukey2g  8143  konigthlem  8190  fpwwe2  8265  wundif  8336  pinn  8502  niex  8505  ltsopi  8512  dmaddpi  8514  dmmulpi  8515  lerelxr  8888  mulnzcnopr  9414  dflt2  10482  expcl2lem  11115  expclzlem  11127  hashun2  11365  fsumss  12198  fsumless  12254  cvgcmpce  12276  rpnnen2lem9  12501  rpnnen2lem11  12503  ramub1lem1  13073  ramub1lem2  13074  isstruct2  13157  structcnvcnv  13159  strleun  13238  strle1  13239  mreexexlem2d  13547  frgpnabllem2  15162  dprdfeq0  15257  dprdss  15264  dprd2da  15277  dmdprdsplit2lem  15280  dpjf  15292  dpjidcl  15293  dpjlid  15296  dpjghm  15298  ablfac1b  15305  ablfac1eulem  15307  ablfac1eu  15308  isdrng2  15522  drngmcl  15525  drngid2  15528  isdrngd  15537  lbspss  15835  lspsolv  15896  lsppratlem1  15900  lsppratlem2  15901  lsppratlem3  15902  lsppratlem4  15903  lspprat  15906  islbs2  15907  islbs3  15908  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  xrs1mnd  16409  xrs10  16410  xrs1cmn  16411  xrge0subm  16412  xrge0cmn  16413  cnmsubglem  16434  expghm  16450  isopn2  16769  clsval2  16787  ntrval2  16788  ntrdif  16789  clsdif  16790  ntrss  16792  cmclsopn  16799  cmntrcld  16800  discld  16826  mretopd  16829  lpsscls  16873  lpss3  16876  restntr  16912  restlp  16913  lpcls  17092  cmpcld  17129  hauscmplem  17133  2ndcsep  17185  1stccnp  17188  hausllycmp  17220  llycmpkgen2  17245  1stckgen  17249  txkgen  17346  qtopcld  17404  qtoprest  17408  qtopcmap  17410  kqdisj  17423  trfil3  17583  isufil2  17603  ufileu  17614  filufint  17615  fixufil  17617  cfinufil  17623  ufinffr  17624  ufilen  17625  fin1aufil  17627  supnfcls  17715  fclscf  17720  flimfnfcls  17723  alexsublem  17738  alexsubALTlem3  17743  cldsubg  17793  imasdsf1olem  17937  blcld  18051  recld2  18320  xrge0gsumle  18338  divcn  18372  cdivcncf  18420  evth  18457  lebnumlem1  18459  lebnumlem2  18460  lebnumlem3  18461  bcthlem2  18747  bcthlem3  18748  bcthlem5  18750  bcth3  18753  ismbl2  18886  cmmbl  18892  nulmbl  18893  nulmbl2  18894  unmbl  18895  shftmbl  18896  volinun  18903  iundisj2  18906  voliunlem1  18907  voliunlem2  18908  volsup  18913  ioombl1lem4  18918  ioombl1  18919  uniiccdif  18933  uniioombllem3  18940  uniioombllem5  18942  uniioombl  18944  uniiccmbl  18945  mbfss  19001  itg1val2  19039  itg1cl  19040  itg1ge0  19041  i1f0  19042  i1f1  19045  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  itg1mulc  19059  itg10a  19065  itg1ge0a  19066  itg1climres  19069  mbfi1fseqlem4  19073  itg2cnlem1  19116  itg2cnlem2  19117  itgss3  19169  itgioo  19170  itgsplitioo  19192  limcdif  19226  ellimc2  19227  limcnlp  19228  ellimc3  19229  limcflflem  19230  limcflf  19231  limcmo  19232  limcmpt2  19234  limcresi  19235  perfdvf  19253  dvreslem  19259  dvres2lem  19260  dvidlem  19265  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvrec  19304  dvcnvlem  19323  dvexp3  19325  dveflem  19326  dvferm1  19332  dvferm2  19334  lhop1lem  19360  lhop  19363  dvcnvrelem2  19365  ftc1lem6  19388  tdeglem4  19446  deg1n0ima  19475  ig1peu  19557  ig1pdvds  19562  aacjcl  19707  taylthlem1  19752  taylthlem2  19753  ulmdvlem3  19779  abelth  19817  logcnlem5  19993  dvlog2  20000  efopnlem2  20004  cxpcn2  20086  sqrcn  20090  rlimcnp  20260  efrlim  20264  jensen  20283  amgm  20285  wilthlem2  20307  dchrelbas2  20476  chebbnd1lem1  20618  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem3  20668  dchrisum0  20669  ballotlemfelz  23049  ballotlemfp1  23050  ballotth  23096  xrge00  23311  iundisj2fi  23364  iundisj2f  23366  gsumpropd2lem  23379  pwsiga  23491  sigainb  23497  measvunilem  23540  measiun  23545  kur14lem6  23742  kur14lem7  23743  cvmscld  23804  umgrass  23871  umgraex  23875  fundmpss  24122  wfi  24207  frind  24243  wfrlem16  24271  relsset  24428  fnsingle  24458  funimage  24467  areacirclem5  24929  prl  25167  islp3  25514  islimrs4  25582  cldbnd  26244  clsun  26246  neibastop2lem  26309  fdc  26455  divrngcl  26588  isdrngo2  26589  isdrngo3  26590  ralxpmap  26761  istopclsd  26775  eldioph2lem2  26840  diophin  26852  setindtr  27117  dnnumch1  27141  dsmmfi  27204  frlmsslss2  27245  frlmlbs  27249  islinds2  27283  lindsind2  27289  lindfrn  27291  islindf4  27308  f1omvdmvd  27386  mvdco  27388  f1omvdconj  27389  pmtrfinv  27402  pmtrfb  27406  pmtrfconj  27407  symggen  27411  symggen2  27412  psgnunilem1  27416  cnmsgngrp  27436  psgnghm2  27438  cntzsdrg  27510  isdomn3  27523  deg1mhm  27526  stoweidlem28  27777  stoweidlem50  27799  stoweidlem57  27806  islsati  29184  lsatfixedN  29199  dochsnkr  31662  hdmaprnlem4tN  32045  hdmap14lem2a  32060
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator