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

Theorem difss 3316
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 3311 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3197 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3162    C_ wss 3165
This theorem is referenced by:  difssd  3317  difss2  3318  ssdifss  3320  disj4  3516  0dif  3538  uneqdifeq  3555  difsnpss  3774  unidif  3875  iunxdif2  3966  difexg  4178  tz7.7  4434  tfi  4660  peano5  4695  reldif  4821  cnvdif  5103  fresaun  5428  fresaunres2  5429  resdif  5510  fndmdif  5645  difxp  6169  oev  6529  oacomf1olem  6578  oelim2  6609  swoer  6704  swoord1  6705  swoord2  6706  boxcutc  6875  undom  6966  domunsncan  6978  sbthlem1  6987  sbthlem2  6988  sbthlem4  6990  sbthlem5  6991  limenpsi  7052  phplem2  7057  php  7061  php3  7063  pssnn  7097  diffi  7105  frfi  7118  fofinf1o  7153  ixpfi2  7170  elfiun  7199  marypha1lem  7202  wemapso  7282  inf3lem3  7347  infdifsn  7373  cantnflem2  7408  dfac8alem  7672  numacn  7692  acnnum  7695  acndom2  7697  inffien  7706  kmlem5  7796  infdif  7851  infdif2  7852  ackbij1lem12  7873  ackbij1lem18  7879  fictb  7887  ssfin4  7952  fin23lem7  7958  fin23lem11  7959  fin23lem26  7967  fin23lem28  7982  fin23lem29  7983  fin23lem30  7984  isf32lem8  8002  compsscnvlem  8012  isf34lem2  8015  compssiso  8016  isf34lem4  8019  enfin1ai  8026  fin1a2lem7  8048  domtriomlem  8084  axcclem  8099  zornn0g  8148  ttukey2g  8159  konigthlem  8206  fpwwe2  8281  wundif  8352  pinn  8518  niex  8521  ltsopi  8528  dmaddpi  8530  dmmulpi  8531  lerelxr  8904  mulnzcnopr  9430  dflt2  10498  expcl2lem  11131  expclzlem  11143  hashun2  11381  fsumss  12214  fsumless  12270  cvgcmpce  12292  rpnnen2lem9  12517  rpnnen2lem11  12519  ramub1lem1  13089  ramub1lem2  13090  isstruct2  13173  structcnvcnv  13175  strleun  13254  strle1  13255  mreexexlem2d  13563  frgpnabllem2  15178  dprdfeq0  15273  dprdss  15280  dprd2da  15293  dmdprdsplit2lem  15296  dpjf  15308  dpjidcl  15309  dpjlid  15312  dpjghm  15314  ablfac1b  15321  ablfac1eulem  15323  ablfac1eu  15324  isdrng2  15538  drngmcl  15541  drngid2  15544  isdrngd  15553  lbspss  15851  lspsolv  15912  lsppratlem1  15916  lsppratlem2  15917  lsppratlem3  15918  lsppratlem4  15919  lspprat  15922  islbs2  15923  islbs3  15924  lbsextlem2  15928  lbsextlem3  15929  lbsextlem4  15930  xrs1mnd  16425  xrs10  16426  xrs1cmn  16427  xrge0subm  16428  xrge0cmn  16429  cnmsubglem  16450  expghm  16466  isopn2  16785  clsval2  16803  ntrval2  16804  ntrdif  16805  clsdif  16806  ntrss  16808  cmclsopn  16815  cmntrcld  16816  discld  16842  mretopd  16845  lpsscls  16889  lpss3  16892  restntr  16928  restlp  16929  lpcls  17108  cmpcld  17145  hauscmplem  17149  2ndcsep  17201  1stccnp  17204  hausllycmp  17236  llycmpkgen2  17261  1stckgen  17265  txkgen  17362  qtopcld  17420  qtoprest  17424  qtopcmap  17426  kqdisj  17439  trfil3  17599  isufil2  17619  ufileu  17630  filufint  17631  fixufil  17633  cfinufil  17639  ufinffr  17640  ufilen  17641  fin1aufil  17643  supnfcls  17731  fclscf  17736  flimfnfcls  17739  alexsublem  17754  alexsubALTlem3  17759  cldsubg  17809  imasdsf1olem  17953  blcld  18067  recld2  18336  xrge0gsumle  18354  divcn  18388  cdivcncf  18436  evth  18473  lebnumlem1  18475  lebnumlem2  18476  lebnumlem3  18477  bcthlem2  18763  bcthlem3  18764  bcthlem5  18766  bcth3  18769  ismbl2  18902  cmmbl  18908  nulmbl  18909  nulmbl2  18910  unmbl  18911  shftmbl  18912  volinun  18919  iundisj2  18922  voliunlem1  18923  voliunlem2  18924  volsup  18929  ioombl1lem4  18934  ioombl1  18935  uniiccdif  18949  uniioombllem3  18956  uniioombllem5  18958  uniioombl  18960  uniiccmbl  18961  mbfss  19017  itg1val2  19055  itg1cl  19056  itg1ge0  19057  i1f0  19058  i1f1  19061  i1fadd  19066  i1fmul  19067  itg1addlem4  19070  itg1addlem5  19071  i1fmulc  19074  itg1mulc  19075  itg10a  19081  itg1ge0a  19082  itg1climres  19085  mbfi1fseqlem4  19089  itg2cnlem1  19132  itg2cnlem2  19133  itgss3  19185  itgioo  19186  itgsplitioo  19208  limcdif  19242  ellimc2  19243  limcnlp  19244  ellimc3  19245  limcflflem  19246  limcflf  19247  limcmo  19248  limcmpt2  19250  limcresi  19251  perfdvf  19269  dvreslem  19275  dvres2lem  19276  dvidlem  19281  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvrec  19320  dvcnvlem  19339  dvexp3  19341  dveflem  19342  dvferm1  19348  dvferm2  19350  lhop1lem  19376  lhop  19379  dvcnvrelem2  19381  ftc1lem6  19404  tdeglem4  19462  deg1n0ima  19491  ig1peu  19573  ig1pdvds  19578  aacjcl  19723  taylthlem1  19768  taylthlem2  19769  ulmdvlem3  19795  abelth  19833  logcnlem5  20009  dvlog2  20016  efopnlem2  20020  cxpcn2  20102  sqrcn  20106  rlimcnp  20276  efrlim  20280  jensen  20299  amgm  20301  wilthlem2  20323  dchrelbas2  20492  chebbnd1lem1  20634  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem3  20684  dchrisum0  20685  ballotlemfelz  23065  ballotlemfp1  23066  ballotth  23112  xrge00  23326  iundisj2fi  23379  iundisj2f  23381  gsumpropd2lem  23394  pwsiga  23506  sigainb  23512  measvunilem  23555  measiun  23560  kur14lem6  23757  kur14lem7  23758  cvmscld  23819  umgrass  23886  umgraex  23890  fundmpss  24193  wfi  24278  frind  24314  wfrlem16  24342  relsset  24499  fnsingle  24529  funimage  24538  areacirclem5  25032  prl  25270  islp3  25617  islimrs4  25685  cldbnd  26347  clsun  26349  neibastop2lem  26412  fdc  26558  divrngcl  26691  isdrngo2  26692  isdrngo3  26693  ralxpmap  26864  istopclsd  26878  eldioph2lem2  26943  diophin  26955  setindtr  27220  dnnumch1  27244  dsmmfi  27307  frlmsslss2  27348  frlmlbs  27352  islinds2  27386  lindsind2  27392  lindfrn  27394  islindf4  27411  f1omvdmvd  27489  mvdco  27491  f1omvdconj  27492  pmtrfinv  27505  pmtrfb  27509  pmtrfconj  27510  symggen  27514  symggen2  27515  psgnunilem1  27519  cnmsgngrp  27539  psgnghm2  27541  cntzsdrg  27613  isdomn3  27626  deg1mhm  27629  stoweidlem28  27880  stoweidlem50  27902  stoweidlem57  27909  islsati  29806  lsatfixedN  29821  dochsnkr  32284  hdmaprnlem4tN  32667  hdmap14lem2a  32682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator