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

Theorem difss 3699
Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
difss (𝐴𝐵) ⊆ 𝐴

Proof of Theorem difss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eldifi 3694 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3572 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cdif 3537  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554
This theorem is referenced by:  difssd  3700  difss2  3701  ssdifss  3703  0dif  3929  disj4  3977  uneqdifeqOLD  4010  difsnpss  4279  unidif  4407  iunxdif2  4504  difexg  4735  reldif  5161  cnvdif  5458  difxp  5477  wfi  5630  tz7.7  5666  fresaun  5988  fresaunres2  5989  resdif  6070  fndmdif  6229  tfi  6945  peano5  6981  wfrlem16  7317  oev  7481  oelim2  7562  swoer  7659  swoord1  7660  swoord2  7661  ralxpmap  7793  boxcutc  7837  undom  7933  domunsncan  7945  sbthlem2  7956  sbthlem4  7958  sbthlem5  7959  limenpsi  8020  phplem2  8025  php  8029  php3  8031  pssnn  8063  diffi  8077  frfi  8090  fofinf1o  8126  ixpfi2  8147  elfiun  8219  marypha1lem  8222  wemapso  8339  infdifsn  8437  cantnflem2  8470  dfac8alem  8735  acnnum  8758  inffien  8769  kmlem5  8859  infdif  8914  infdif2  8915  ackbij1lem18  8942  fictb  8950  fin23lem7  9021  fin23lem11  9022  fin23lem28  9045  fin23lem30  9047  compsscnvlem  9075  isf34lem2  9078  compssiso  9079  isf34lem4  9082  fin1a2lem7  9111  domtriomlem  9147  axcclem  9162  zornn0g  9210  ttukey2g  9221  konigthlem  9269  pinn  9579  niex  9582  ltsopi  9589  dmaddpi  9591  dmmulpi  9592  lerelxr  9980  mulnzcnopr  10552  dflt2  11857  expcl2lem  12734  expclzlem  12746  hashun2  13033  fsumss  14303  fsumless  14369  cvgcmpce  14391  fprodss  14517  rpnnen2lem9  14790  isstruct2  15704  structcnvcnv  15706  fsets  15723  strleun  15799  strle1  15800  mreexexlem2d  16128  gsumpropd2lem  17096  symgfixf1  17680  f1omvdmvd  17686  mvdco  17688  f1omvdconj  17689  pmtrfb  17708  pmtrfconj  17709  symggen  17713  symggen2  17714  psgnunilem1  17736  frgpnabllem2  18100  dprdss  18251  dprd2da  18264  dmdprdsplit2lem  18267  dpjidcl  18280  ablfac1b  18292  ablfac1eu  18295  isdrng2  18580  drngmcl  18583  drngid2  18586  isdrngd  18595  xrs1mnd  19603  xrs10  19604  xrs1cmn  19605  xrge0subm  19606  xrge0cmn  19607  cnmgpid  19627  cnmsubglem  19628  expghm  19663  cnmsgngrp  19744  psgninv  19747  dsmmfi  19901  islinds2  19971  lindsind2  19977  lindfrn  19979  islindf4  19996  mdetdiaglem  20223  mdetrsca2  20229  mdetrlin2  20232  mdetralt  20233  mdetunilem5  20241  mdetunilem9  20245  maducoeval2  20265  smadiadetglem1  20296  isopn2  20646  ntrval2  20665  ntrdif  20666  clsdif  20667  ntrss  20669  cmclsopn  20676  discld  20703  mretopd  20706  lpsscls  20755  restntr  20796  cmpcld  21015  2ndcsep  21072  1stccnp  21075  llycmpkgen2  21163  1stckgen  21167  txkgen  21265  qtopcld  21326  qtopcmap  21332  kqdisj  21345  isufil2  21522  ufileu  21533  filufint  21534  fixufil  21536  cfinufil  21542  ufilen  21544  fin1aufil  21546  supnfcls  21634  flimfnfcls  21642  alexsublem  21658  alexsubALTlem3  21663  cldsubg  21724  imasdsf1olem  21988  recld2  22425  sszcld  22428  xrge0gsumle  22444  divcn  22479  cdivcncf  22528  bcth3  22936  ismbl2  23102  cmmbl  23109  nulmbl  23110  nulmbl2  23111  unmbl  23112  voliunlem1  23125  voliunlem2  23126  ioombl1lem4  23136  ioombl1  23137  uniioombllem3  23159  mbfss  23219  itg1cl  23258  itg1ge0  23259  i1f0  23260  i1f1  23263  i1fmul  23269  itg1addlem4  23272  itg1mulc  23277  itg10a  23283  itg1ge0a  23284  itg1climres  23287  itg2cnlem1  23334  itgioo  23388  itgsplitioo  23410  limcdif  23446  ellimc2  23447  ellimc3  23449  limcflflem  23450  limcflf  23451  limcmo  23452  limcresi  23455  dvreslem  23479  dvres2lem  23480  dvidlem  23485  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvrec  23524  dvcnvlem  23543  lhop1lem  23580  lhop  23583  tdeglem4  23624  deg1n0ima  23653  aacjcl  23886  taylthlem2  23932  abelth  23999  logcnlem5  24192  dvlog2  24199  efopnlem2  24203  dvcncxp1  24284  dvcnsqrt  24285  cxpcn2  24287  sqrtcn  24291  efrlim  24496  jensen  24515  amgm  24517  lgamgulmlem2  24556  lgamucov  24564  wilthlem2  24595  dchrelbas2  24762  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem3  25008  dchrisum0  25009  tgisline  25322  upgrss  25755  umgrass  25848  frgrawopreg2  26578  xrge00  29017  submatres  29200  madjusmdetlem2  29222  madjusmdetlem3  29223  qtophaus  29231  fsumcvg4  29324  gsumesum  29448  pwsiga  29520  sigainb  29526  carsggect  29707  omsmeas  29712  sitgclg  29731  ballotlemfelz  29879  ballotlemfp1  29880  ballotth  29926  kur14lem6  30447  kur14lem7  30448  cvmscld  30509  mclsppslem  30734  fundmpss  30910  frind  30984  relsset  31165  limitssson  31188  fnsingle  31196  funimage  31205  cldbnd  31491  clsun  31493  topdifinffinlem  32371  matunitlindflem1  32575  poimirlem8  32587  poimirlem26  32605  poimirlem30  32609  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  voliunnfl  32623  cnambfre  32628  dvtan  32630  dvasin  32666  dvacos  32667  areacirclem4  32673  fdc  32711  divrngcl  32926  isdrngo2  32927  isdrngo3  32928  islsati  33299  hdmap14lem2a  36177  istopclsd  36281  diophin  36354  dnnumch1  36632  cntzsdrg  36791  isdomn3  36801  deg1mhm  36804  gneispace  37452  sumnnodd  38697  cncficcgt0  38774  cncfiooicclem1  38779  cxpcncf2  38786  dirkercncflem2  38997  fourierdlem62  39061  fourierdlem66  39065  fourierdlem68  39067  fourierdlem95  39094  etransclem24  39151  etransclem44  39171  gsumge0cl  39264  sge0fodjrnlem  39309  carageniuncllem1  39411  smfresal  39673  frgrwopreg2  41488  lindslinindimp2lem2  42042  amgmlemALT  42358
  Copyright terms: Public domain W3C validator