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

Theorem difss 3466
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 3461 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3344 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3309    C_ wss 3312
This theorem is referenced by:  difssd  3467  difss2  3468  ssdifss  3470  disj4  3668  0dif  3691  uneqdifeq  3708  difsnpss  3933  unidif  4039  iunxdif2  4131  difexg  4343  tz7.7  4599  tfi  4824  peano5  4859  reldif  4985  cnvdif  5269  fresaun  5605  fresaunres2  5606  resdif  5687  fndmdif  5825  difxp  6371  oev  6749  oelim2  6829  swoer  6924  swoord1  6925  swoord2  6926  boxcutc  7096  undom  7187  domunsncan  7199  sbthlem2  7209  sbthlem4  7211  sbthlem5  7212  limenpsi  7273  phplem2  7278  php  7282  php3  7284  pssnn  7318  diffi  7330  frfi  7343  fofinf1o  7378  ixpfi2  7396  elfiun  7426  marypha1lem  7429  wemapso  7509  inf3lem3  7574  infdifsn  7600  cantnflem2  7635  dfac8alem  7899  acnnum  7922  inffien  7933  kmlem5  8023  infdif  8078  infdif2  8079  ackbij1lem18  8106  fictb  8114  fin23lem7  8185  fin23lem11  8186  fin23lem28  8209  fin23lem30  8211  compsscnvlem  8239  isf34lem2  8242  compssiso  8243  isf34lem4  8246  fin1a2lem7  8275  domtriomlem  8311  axcclem  8326  zornn0g  8374  ttukey2g  8385  konigthlem  8432  pinn  8744  niex  8747  ltsopi  8754  dmaddpi  8756  dmmulpi  8757  lerelxr  9130  mulnzcnopr  9657  dflt2  10730  expcl2lem  11381  expclzlem  11393  hashun2  11645  fsumss  12507  fsumless  12563  cvgcmpce  12585  rpnnen2lem9  12810  isstruct2  13466  structcnvcnv  13468  strleun  13547  strle1  13548  mreexexlem2d  13858  frgpnabllem2  15473  dprdss  15575  dprd2da  15588  dmdprdsplit2lem  15591  dpjidcl  15604  ablfac1b  15616  ablfac1eu  15619  isdrng2  15833  drngmcl  15836  drngid2  15839  isdrngd  15848  xrs1mnd  16724  xrs10  16725  xrs1cmn  16726  xrge0subm  16727  xrge0cmn  16728  cnmsubglem  16749  expghm  16765  isopn2  17084  ntrval2  17103  ntrdif  17104  clsdif  17105  ntrss  17107  cmclsopn  17114  cmntrcld  17115  discld  17141  mretopd  17144  lpsscls  17193  islp3  17198  restntr  17234  cmpcld  17453  2ndcsep  17510  1stccnp  17513  llycmpkgen2  17570  1stckgen  17574  txkgen  17672  qtopcld  17733  qtopcmap  17739  kqdisj  17752  isufil2  17928  ufileu  17939  filufint  17940  fixufil  17942  cfinufil  17948  ufilen  17950  fin1aufil  17952  supnfcls  18040  flimfnfcls  18048  alexsublem  18063  alexsubALTlem3  18068  cldsubg  18128  imasdsf1olem  18391  recld2  18833  sszcld  18836  xrge0gsumle  18852  divcn  18886  cdivcncf  18935  bcth3  19272  ismbl2  19411  cmmbl  19417  nulmbl  19418  nulmbl2  19419  unmbl  19420  voliunlem1  19432  voliunlem2  19433  ioombl1lem4  19443  ioombl1  19444  uniioombllem3  19465  mbfss  19526  itg1cl  19565  itg1ge0  19566  i1f0  19567  i1f1  19570  i1fmul  19576  itg1addlem4  19579  itg1mulc  19584  itg10a  19590  itg1ge0a  19591  itg1climres  19594  itg2cnlem1  19641  itgioo  19695  itgsplitioo  19717  limcdif  19751  ellimc2  19752  ellimc3  19754  limcflflem  19755  limcflf  19756  limcmo  19757  limcresi  19760  dvreslem  19784  dvres2lem  19785  dvidlem  19790  dvcnp2  19794  dvaddbr  19812  dvmulbr  19813  dvcobr  19820  dvrec  19829  dvcnvlem  19848  lhop1lem  19885  lhop  19888  tdeglem4  19971  deg1n0ima  20000  aacjcl  20232  taylthlem2  20278  abelth  20345  logcnlem5  20525  dvlog2  20532  efopnlem2  20536  cxpcn2  20618  sqrcn  20622  efrlim  20796  jensen  20815  amgm  20817  wilthlem2  20840  dchrelbas2  21009  rpvmasum2  21194  dchrisum0re  21195  dchrisum0lem3  21201  dchrisum0  21202  umgrass  21342  xrge00  24196  gsumpropd2lem  24208  gsumesum  24439  pwsiga  24501  sigainb  24507  sibfof  24642  sitgclg  24644  ballotlemfelz  24736  ballotlemfp1  24737  ballotth  24783  lgamgulmlem2  24802  lgamucov  24810  kur14lem6  24885  kur14lem7  24886  cvmscld  24948  fprodss  25263  fundmpss  25377  wfi  25462  frind  25498  wfrlem16  25526  relsset  25683  fnsingle  25714  funimage  25723  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  voliunnfl  26196  cnambfre  26201  areacirclem5  26232  cldbnd  26266  clsun  26268  fdc  26386  divrngcl  26510  isdrngo2  26511  isdrngo3  26512  ralxpmap  26679  istopclsd  26691  diophin  26768  setindtr  27032  dnnumch1  27056  dsmmfi  27119  islinds2  27198  lindsind2  27204  lindfrn  27206  islindf4  27223  f1omvdmvd  27301  mvdco  27303  f1omvdconj  27304  pmtrfb  27321  pmtrfconj  27322  symggen  27326  symggen2  27327  psgnunilem1  27331  cnmsgngrp  27351  psgnghm2  27353  cntzsdrg  27425  isdomn3  27438  deg1mhm  27441  frgrawopreg2  28298  islsati  29631  hdmap14lem2a  32507
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator