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

Theorem difss 3460
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 3455 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3338 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3303    C_ wss 3306
This theorem is referenced by:  difssd  3461  difss2  3462  ssdifss  3464  disj4  3700  0dif  3723  uneqdifeq  3740  difsnpss  3965  unidif  4071  iunxdif2  4163  difexg  4380  tz7.7  4636  tfi  4862  peano5  4897  reldif  5023  cnvdif  5307  fresaun  5643  fresaunres2  5644  resdif  5725  fndmdif  5863  difxp  6409  oev  6787  oelim2  6867  swoer  6962  swoord1  6963  swoord2  6964  boxcutc  7134  undom  7225  domunsncan  7237  sbthlem2  7247  sbthlem4  7249  sbthlem5  7250  limenpsi  7311  phplem2  7316  php  7320  php3  7322  pssnn  7356  diffi  7368  frfi  7381  fofinf1o  7416  ixpfi2  7434  elfiun  7464  marypha1lem  7467  wemapso  7549  inf3lem3  7614  infdifsn  7640  cantnflem2  7675  dfac8alem  7941  acnnum  7964  inffien  7975  kmlem5  8065  infdif  8120  infdif2  8121  ackbij1lem18  8148  fictb  8156  fin23lem7  8227  fin23lem11  8228  fin23lem28  8251  fin23lem30  8253  compsscnvlem  8281  isf34lem2  8284  compssiso  8285  isf34lem4  8288  fin1a2lem7  8317  domtriomlem  8353  axcclem  8368  zornn0g  8416  ttukey2g  8427  konigthlem  8474  pinn  8786  niex  8789  ltsopi  8796  dmaddpi  8798  dmmulpi  8799  lerelxr  9172  mulnzcnopr  9699  dflt2  10772  expcl2lem  11424  expclzlem  11436  hashun2  11688  fsumss  12550  fsumless  12606  cvgcmpce  12628  rpnnen2lem9  12853  isstruct2  13509  structcnvcnv  13511  strleun  13590  strle1  13591  mreexexlem2d  13901  frgpnabllem2  15516  dprdss  15618  dprd2da  15631  dmdprdsplit2lem  15634  dpjidcl  15647  ablfac1b  15659  ablfac1eu  15662  isdrng2  15876  drngmcl  15879  drngid2  15882  isdrngd  15891  xrs1mnd  16767  xrs10  16768  xrs1cmn  16769  xrge0subm  16770  xrge0cmn  16771  cnmsubglem  16792  expghm  16808  isopn2  17127  ntrval2  17146  ntrdif  17147  clsdif  17148  ntrss  17150  cmclsopn  17157  cmntrcld  17158  discld  17184  mretopd  17187  lpsscls  17236  islp3  17241  restntr  17277  cmpcld  17496  2ndcsep  17553  1stccnp  17556  llycmpkgen2  17613  1stckgen  17617  txkgen  17715  qtopcld  17776  qtopcmap  17782  kqdisj  17795  isufil2  17971  ufileu  17982  filufint  17983  fixufil  17985  cfinufil  17991  ufilen  17993  fin1aufil  17995  supnfcls  18083  flimfnfcls  18091  alexsublem  18106  alexsubALTlem3  18111  cldsubg  18171  imasdsf1olem  18434  recld2  18876  sszcld  18879  xrge0gsumle  18895  divcn  18929  cdivcncf  18978  bcth3  19315  ismbl2  19454  cmmbl  19460  nulmbl  19461  nulmbl2  19462  unmbl  19463  voliunlem1  19475  voliunlem2  19476  ioombl1lem4  19486  ioombl1  19487  uniioombllem3  19508  mbfss  19567  itg1cl  19606  itg1ge0  19607  i1f0  19608  i1f1  19611  i1fmul  19617  itg1addlem4  19620  itg1mulc  19625  itg10a  19631  itg1ge0a  19632  itg1climres  19635  itg2cnlem1  19682  itgioo  19736  itgsplitioo  19758  limcdif  19794  ellimc2  19795  ellimc3  19797  limcflflem  19798  limcflf  19799  limcmo  19800  limcresi  19803  dvreslem  19827  dvres2lem  19828  dvidlem  19833  dvcnp2  19837  dvaddbr  19855  dvmulbr  19856  dvcobr  19863  dvrec  19872  dvcnvlem  19891  lhop1lem  19928  lhop  19931  tdeglem4  20014  deg1n0ima  20043  aacjcl  20275  taylthlem2  20321  abelth  20388  logcnlem5  20568  dvlog2  20575  efopnlem2  20579  cxpcn2  20661  sqrcn  20665  efrlim  20839  jensen  20858  amgm  20860  wilthlem2  20883  dchrelbas2  21052  rpvmasum2  21237  dchrisum0re  21238  dchrisum0lem3  21244  dchrisum0  21245  umgrass  21385  xrge00  24239  gsumpropd2lem  24251  gsumesum  24482  pwsiga  24544  sigainb  24550  sibfof  24685  sitgclg  24687  ballotlemfelz  24779  ballotlemfp1  24780  ballotth  24826  lgamgulmlem2  24845  lgamucov  24853  kur14lem6  24928  kur14lem7  24929  cvmscld  24991  fprodss  25305  fundmpss  25421  wfi  25513  frind  25549  wfrlem16  25584  relsset  25764  limitssson  25787  fnsingle  25795  funimage  25804  mblfinlem3  26281  mblfinlem4  26282  ismblfin  26283  voliunnfl  26286  cnambfre  26291  dvtan  26293  areacirclem4  26333  cldbnd  26367  clsun  26369  fdc  26487  divrngcl  26611  isdrngo2  26612  isdrngo3  26613  ralxpmap  26780  istopclsd  26792  diophin  26869  setindtr  27133  dnnumch1  27157  dsmmfi  27219  islinds2  27298  lindsind2  27304  lindfrn  27306  islindf4  27323  f1omvdmvd  27401  mvdco  27403  f1omvdconj  27404  pmtrfb  27421  pmtrfconj  27422  symggen  27426  symggen2  27427  psgnunilem1  27431  cnmsgngrp  27451  psgnghm2  27453  cntzsdrg  27525  isdomn3  27538  deg1mhm  27541  frgrawopreg2  28538  islsati  29890  hdmap14lem2a  32766
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-dif 3309  df-in 3313  df-ss 3320
  Copyright terms: Public domain W3C validator