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

Theorem difss 3410
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 3405 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3288 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3253    C_ wss 3256
This theorem is referenced by:  difssd  3411  difss2  3412  ssdifss  3414  disj4  3612  0dif  3635  uneqdifeq  3652  difsnpss  3877  unidif  3982  iunxdif2  4073  difexg  4285  tz7.7  4541  tfi  4766  peano5  4801  reldif  4927  cnvdif  5211  fresaun  5547  fresaunres2  5548  resdif  5629  fndmdif  5766  difxp  6312  oev  6687  oelim2  6767  swoer  6862  swoord1  6863  swoord2  6864  boxcutc  7034  undom  7125  domunsncan  7137  sbthlem2  7147  sbthlem4  7149  sbthlem5  7150  limenpsi  7211  phplem2  7216  php  7220  php3  7222  pssnn  7256  diffi  7268  frfi  7281  fofinf1o  7316  ixpfi2  7333  elfiun  7363  marypha1lem  7366  wemapso  7446  inf3lem3  7511  infdifsn  7537  cantnflem2  7572  dfac8alem  7836  acnnum  7859  inffien  7870  kmlem5  7960  infdif  8015  infdif2  8016  ackbij1lem18  8043  fictb  8051  fin23lem7  8122  fin23lem11  8123  fin23lem28  8146  fin23lem30  8148  compsscnvlem  8176  isf34lem2  8179  compssiso  8180  isf34lem4  8183  fin1a2lem7  8212  domtriomlem  8248  axcclem  8263  zornn0g  8311  ttukey2g  8322  konigthlem  8369  pinn  8681  niex  8684  ltsopi  8691  dmaddpi  8693  dmmulpi  8694  lerelxr  9067  mulnzcnopr  9593  dflt2  10666  expcl2lem  11313  expclzlem  11325  hashun2  11577  fsumss  12439  fsumless  12495  cvgcmpce  12517  rpnnen2lem9  12742  isstruct2  13398  structcnvcnv  13400  strleun  13479  strle1  13480  mreexexlem2d  13790  frgpnabllem2  15405  dprdss  15507  dprd2da  15520  dmdprdsplit2lem  15523  dpjidcl  15536  ablfac1b  15548  ablfac1eu  15551  isdrng2  15765  drngmcl  15768  drngid2  15771  isdrngd  15780  xrs1mnd  16652  xrs10  16653  xrs1cmn  16654  xrge0subm  16655  xrge0cmn  16656  cnmsubglem  16677  expghm  16693  isopn2  17012  ntrval2  17031  ntrdif  17032  clsdif  17033  ntrss  17035  cmclsopn  17042  cmntrcld  17043  discld  17069  mretopd  17072  lpsscls  17121  restntr  17161  cmpcld  17380  2ndcsep  17436  1stccnp  17439  llycmpkgen2  17496  1stckgen  17500  txkgen  17598  qtopcld  17659  qtopcmap  17665  kqdisj  17678  isufil2  17854  ufileu  17865  filufint  17866  fixufil  17868  cfinufil  17874  ufilen  17876  fin1aufil  17878  supnfcls  17966  flimfnfcls  17974  alexsublem  17989  alexsubALTlem3  17994  cldsubg  18054  imasdsf1olem  18304  recld2  18709  sszcld  18712  xrge0gsumle  18728  divcn  18762  cdivcncf  18811  bcth3  19146  ismbl2  19283  cmmbl  19289  nulmbl  19290  nulmbl2  19291  unmbl  19292  voliunlem1  19304  voliunlem2  19305  ioombl1lem4  19315  ioombl1  19316  uniioombllem3  19337  mbfss  19398  itg1cl  19437  itg1ge0  19438  i1f0  19439  i1f1  19442  i1fmul  19448  itg1addlem4  19451  itg1mulc  19456  itg10a  19462  itg1ge0a  19463  itg1climres  19466  itg2cnlem1  19513  itgioo  19567  itgsplitioo  19589  limcdif  19623  ellimc2  19624  ellimc3  19626  limcflflem  19627  limcflf  19628  limcmo  19629  limcresi  19632  dvreslem  19656  dvres2lem  19657  dvidlem  19662  dvcnp2  19666  dvaddbr  19684  dvmulbr  19685  dvcobr  19692  dvrec  19701  dvcnvlem  19720  lhop1lem  19757  lhop  19760  tdeglem4  19843  deg1n0ima  19872  aacjcl  20104  taylthlem2  20150  abelth  20217  logcnlem5  20397  dvlog2  20404  efopnlem2  20408  cxpcn2  20490  sqrcn  20494  efrlim  20668  jensen  20687  amgm  20689  wilthlem2  20712  dchrelbas2  20881  rpvmasum2  21066  dchrisum0re  21067  dchrisum0lem3  21073  dchrisum0  21074  umgrass  21214  xrge00  24030  gsumpropd2lem  24042  gsumesum  24240  pwsiga  24302  sigainb  24308  ballotlemfelz  24520  ballotlemfp1  24521  ballotth  24567  lgamgulmlem2  24586  lgamucov  24594  kur14lem6  24669  kur14lem7  24670  cvmscld  24732  fprodss  25046  fundmpss  25139  wfi  25224  frind  25260  wfrlem16  25288  relsset  25445  fnsingle  25475  funimage  25484  voliunnfl  25948  areacirclem5  25979  cldbnd  26013  clsun  26015  fdc  26133  divrngcl  26257  isdrngo2  26258  isdrngo3  26259  ralxpmap  26426  istopclsd  26438  diophin  26515  setindtr  26779  dnnumch1  26803  dsmmfi  26866  islinds2  26945  lindsind2  26951  lindfrn  26953  islindf4  26970  f1omvdmvd  27048  mvdco  27050  f1omvdconj  27051  pmtrfb  27068  pmtrfconj  27069  symggen  27073  symggen2  27074  psgnunilem1  27078  cnmsgngrp  27098  psgnghm2  27100  cntzsdrg  27172  isdomn3  27185  deg1mhm  27188  frgrawopreg2  27796  islsati  29160  hdmap14lem2a  32036
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-dif 3259  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator