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

Theorem difss 3220
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 3215 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3105 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3075    C_ wss 3078
This theorem is referenced by:  ssdifss  3221  disj4  3410  0dif  3431  uneqdifeq  3448  unidif  3757  iunxdif2  3848  difexg  4058  tz7.7  4311  tfi  4535  peano5  4570  reldif  4712  cnvdif  4994  fresaun  5269  fresaunres2  5270  resdif  5351  fndmdif  5481  difxp  6005  oev  6399  oacomf1olem  6448  oelim2  6479  swoer  6574  swoord1  6575  swoord2  6576  boxcutc  6745  undom  6835  domunsncan  6847  sbthlem1  6856  sbthlem2  6857  sbthlem4  6859  sbthlem5  6860  limenpsi  6921  phplem2  6926  php  6930  php3  6932  pssnn  6966  diffi  6974  frfi  6987  fofinf1o  7022  ixpfi2  7038  elfiun  7067  marypha1lem  7070  wemapso  7150  inf3lem3  7215  infdifsn  7241  cantnflem2  7276  dfac8alem  7540  numacn  7560  acnnum  7563  acndom2  7565  inffien  7574  kmlem5  7664  infdif  7719  infdif2  7720  ackbij1lem12  7741  ackbij1lem18  7747  fictb  7755  ssfin4  7820  fin23lem7  7826  fin23lem11  7827  fin23lem26  7835  fin23lem28  7850  fin23lem29  7851  fin23lem30  7852  isf32lem8  7870  compsscnvlem  7880  isf34lem2  7883  compssiso  7884  isf34lem4  7887  enfin1ai  7894  fin1a2lem7  7916  domtriomlem  7952  axcclem  7967  zornn0g  8016  ttukey2g  8027  konigthlem  8070  fpwwe2  8145  wundif  8216  pinn  8382  niex  8385  ltsopi  8392  dmaddpi  8394  dmmulpi  8395  lerelxr  8768  mulnzcnopr  9294  dflt2  10361  expcl2lem  10993  expclzlem  11005  hashun2  11243  fsumss  12075  fsumless  12131  cvgcmpce  12153  rpnnen2lem9  12375  rpnnen2lem11  12377  ramub1lem1  12947  ramub1lem2  12948  isstruct2  13031  structcnvcnv  13033  strleun  13112  strle1  13113  frgpnabllem2  14997  dprdfeq0  15092  dprdss  15099  dprd2da  15112  dmdprdsplit2lem  15115  dpjf  15127  dpjidcl  15128  dpjlid  15131  dpjghm  15133  ablfac1b  15140  ablfac1eulem  15142  ablfac1eu  15143  isdrng2  15357  drngmcl  15360  drngid2  15363  isdrngd  15372  lbspss  15670  lspsolv  15731  lsppratlem1  15734  lsppratlem2  15735  lsppratlem3  15736  lsppratlem4  15737  lspprat  15740  islbs2  15741  islbs3  15742  lbsextlem2  15744  lbsextlem3  15745  lbsextlem4  15746  xrs1mnd  16241  xrs10  16242  xrs1cmn  16243  xrge0subm  16244  xrge0cmn  16245  cnmsubglem  16266  expghm  16282  isopn2  16601  clsval2  16619  ntrval2  16620  ntrdif  16621  clsdif  16622  ntrss  16624  cmclsopn  16631  cmntrcld  16632  discld  16658  mretopd  16661  lpsscls  16705  lpss3  16708  restntr  16744  restlp  16745  lpcls  16924  cmpcld  16961  hauscmplem  16965  2ndcsep  17017  1stccnp  17020  hausllycmp  17052  llycmpkgen2  17077  1stckgen  17081  txkgen  17178  qtopcld  17236  qtoprest  17240  qtopcmap  17242  kqdisj  17255  trfil3  17415  isufil2  17435  ufileu  17446  filufint  17447  fixufil  17449  cfinufil  17455  ufinffr  17456  ufilen  17457  fin1aufil  17459  supnfcls  17547  fclscf  17552  flimfnfcls  17555  alexsublem  17570  alexsubALTlem3  17575  cldsubg  17625  imasdsf1olem  17769  blcld  17883  recld2  18152  xrge0gsumle  18170  divcn  18204  cdivcncf  18252  evth  18289  lebnumlem1  18291  lebnumlem2  18292  lebnumlem3  18293  bcthlem2  18579  bcthlem3  18580  bcthlem5  18582  bcth3  18585  ismbl2  18718  cmmbl  18724  nulmbl  18725  nulmbl2  18726  unmbl  18727  shftmbl  18728  volinun  18735  iundisj2  18738  voliunlem1  18739  voliunlem2  18740  volsup  18745  ioombl1lem4  18750  ioombl1  18751  uniiccdif  18765  uniioombllem3  18772  uniioombllem5  18774  uniioombl  18776  uniiccmbl  18777  mbfss  18833  itg1val2  18871  itg1cl  18872  itg1ge0  18873  i1f0  18874  i1f1  18877  i1fadd  18882  i1fmul  18883  itg1addlem4  18886  itg1addlem5  18887  i1fmulc  18890  itg1mulc  18891  itg10a  18897  itg1ge0a  18898  itg1climres  18901  mbfi1fseqlem4  18905  itg2cnlem1  18948  itg2cnlem2  18949  itgss3  19001  itgioo  19002  itgsplitioo  19024  limcdif  19058  ellimc2  19059  limcnlp  19060  ellimc3  19061  limcflflem  19062  limcflf  19063  limcmo  19064  limcmpt2  19066  limcresi  19067  perfdvf  19085  dvreslem  19091  dvres2lem  19092  dvidlem  19097  dvcnp2  19101  dvaddbr  19119  dvmulbr  19120  dvcobr  19127  dvrec  19136  dvcnvlem  19155  dvexp3  19157  dveflem  19158  dvferm1  19164  dvferm2  19166  lhop1lem  19192  lhop  19195  dvcnvrelem2  19197  ftc1lem6  19220  tdeglem4  19278  deg1n0ima  19307  ig1peu  19389  ig1pdvds  19394  aacjcl  19539  taylthlem1  19584  taylthlem2  19585  ulmdvlem3  19611  abelth  19649  logcnlem5  19825  dvlog2  19832  efopnlem2  19836  cxpcn2  19954  sqrcn  19958  rlimcnp  20092  efrlim  20096  jensen  20115  amgm  20117  wilthlem2  20139  dchrelbas2  20308  chebbnd1lem1  20450  rpvmasum2  20493  dchrisum0re  20494  dchrisum0lem3  20500  dchrisum0  20501  kur14lem6  22913  kur14lem7  22914  cvmscld  22975  umgrass  23042  umgraex  23046  fundmpss  23290  wfi  23375  frind  23411  wfrlem16  23439  relsset  23603  fnsingle  23632  funimage  23641  prl  24333  islp3  24680  islimrs4  24748  cldbnd  25410  clsun  25412  neibastop2lem  25475  fdc  25621  divrngcl  25754  isdrngo2  25755  isdrngo3  25756  ralxpmap  25927  istopclsd  25941  eldioph2lem2  26006  diophin  26018  setindtr  26283  dnnumch1  26307  dsmmfi  26370  frlmsslss2  26411  frlmlbs  26415  islinds2  26449  lindsind2  26455  lindfrn  26457  islindf4  26474  f1omvdmvd  26552  mvdco  26554  f1omvdconj  26555  pmtrfinv  26568  pmtrfb  26572  pmtrfconj  26573  symggen  26577  symggen2  26578  psgnunilem1  26582  cnmsgngrp  26602  psgnghm2  26604  cntzsdrg  26676  isdomn3  26689  deg1mhm  26692  islsati  27943  lsatfixedN  27958  dochsnkr  30421  hdmaprnlem4tN  30804  hdmap14lem2a  30819
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator