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

Theorem difss 3886
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 3881 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3754 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cdif 3718  wss 3721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-dif 3724  df-in 3728  df-ss 3735
This theorem is referenced by:  difssd  3887  difss2  3888  ssdifss  3890  0dif  4119  disj4  4167  difsnpss  4471  unidif  4605  iunxdif2  4700  difexg  4939  reldif  5377  cnvdif  5680  difxp  5699  wfi  5856  tz7.7  5892  fresaun  6215  fresaunres2  6216  resdif  6298  fndmdif  6464  tfi  7199  peano5  7235  wfrlem16  7582  oev  7747  oelim2  7828  swoer  7925  swoord1  7926  swoord2  7927  ralxpmap  8060  boxcutc  8104  undom  8203  domunsncan  8215  sbthlem2  8226  sbthlem4  8228  sbthlem5  8229  limenpsi  8290  phplem2  8295  php  8299  php3  8301  pssnn  8333  diffi  8347  frfi  8360  fofinf1o  8396  ixpfi2  8419  elfiun  8491  marypha1lem  8494  wemapso  8611  infdifsn  8717  cantnflem2  8750  dfac8alem  9051  acnnum  9074  inffien  9085  kmlem5  9177  infdif  9232  infdif2  9233  ackbij1lem18  9260  fictb  9268  fin23lem7  9339  fin23lem11  9340  fin23lem28  9363  fin23lem30  9365  compsscnvlem  9393  isf34lem2  9396  compssiso  9397  isf34lem4  9400  fin1a2lem7  9429  domtriomlem  9465  axcclem  9480  zornn0g  9528  ttukey2g  9539  konigthlem  9591  pinn  9901  niex  9904  ltsopi  9911  dmaddpi  9913  dmmulpi  9914  lerelxr  10302  mulnzcnopr  10874  dflt2  12185  expcl2lem  13078  expclzlem  13090  hashun2  13373  fsumss  14663  fsumless  14734  cvgcmpce  14756  fprodss  14884  rpnnen2lem9  15156  isstruct2  16073  structcnvcnv  16077  fsets  16097  strleun  16179  strle1  16180  mreexexlem2d  16512  gsumpropd2lem  17480  symgfixf1  18063  f1omvdmvd  18069  mvdco  18071  f1omvdconj  18072  pmtrfb  18091  pmtrfconj  18092  symggen  18096  symggen2  18097  psgnunilem1  18119  frgpnabllem2  18483  dprdss  18635  dprd2da  18648  dmdprdsplit2lem  18651  dpjidcl  18664  ablfac1b  18676  ablfac1eu  18679  isdrng2  18966  drngmcl  18969  drngid2  18972  isdrngd  18981  xrs1mnd  19998  xrs10  19999  xrs1cmn  20000  xrge0subm  20001  xrge0cmn  20002  cnmgpid  20022  cnmsubglem  20023  expghm  20058  cnmsgngrp  20139  psgninv  20142  dsmmfi  20298  islinds2  20368  lindsind2  20374  lindfrn  20376  islindf4  20393  mdetdiaglem  20621  mdetrsca2  20627  mdetrlin2  20630  mdetralt  20631  mdetunilem5  20639  mdetunilem9  20643  maducoeval2  20663  smadiadetglem1  20695  isopn2  21056  ntrval2  21075  ntrdif  21076  clsdif  21077  ntrss  21079  cmclsopn  21086  discld  21113  mretopd  21116  lpsscls  21165  restntr  21206  cmpcld  21425  2ndcsep  21482  1stccnp  21485  llycmpkgen2  21573  1stckgen  21577  txkgen  21675  qtopcld  21736  qtopcmap  21742  kqdisj  21755  isufil2  21931  ufileu  21942  filufint  21943  fixufil  21945  cfinufil  21951  ufilen  21953  fin1aufil  21955  supnfcls  22043  flimfnfcls  22051  alexsublem  22067  alexsubALTlem3  22072  cldsubg  22133  imasdsf1olem  22397  recld2  22836  sszcld  22839  xrge0gsumle  22855  divcn  22890  cdivcncf  22939  bcth3  23346  ismbl2  23514  cmmbl  23521  nulmbl  23522  nulmbl2  23523  unmbl  23524  voliunlem1  23537  voliunlem2  23538  ioombl1lem4  23548  ioombl1  23549  uniioombllem3  23572  mbfss  23632  itg1cl  23671  itg1ge0  23672  i1f0  23673  i1f1  23676  i1fmul  23682  itg1addlem4  23685  itg1mulc  23690  itg10a  23696  itg1ge0a  23697  itg1climres  23700  itg2cnlem1  23747  itgioo  23801  itgsplitioo  23823  limcdif  23859  ellimc2  23860  ellimc3  23862  limcflflem  23863  limcflf  23864  limcmo  23865  limcresi  23868  dvreslem  23892  dvres2lem  23893  dvidlem  23898  dvcnp2  23902  dvaddbr  23920  dvmulbr  23921  dvcobr  23928  dvrec  23937  dvcnvlem  23958  lhop1lem  23995  lhop  23998  tdeglem4  24039  deg1n0ima  24068  aacjcl  24301  taylthlem2  24347  abelth  24414  logcnlem5  24612  dvlog2  24619  efopnlem2  24623  dvcncxp1  24704  dvcnsqrt  24705  cxpcn2  24707  sqrtcn  24711  efrlim  24916  jensen  24935  amgm  24937  lgamgulmlem2  24976  lgamucov  24984  wilthlem2  25015  dchrelbas2  25182  rpvmasum2  25421  dchrisum0re  25422  dchrisum0lem3  25428  dchrisum0  25429  tgisline  25742  upgrss  26203  frgrwopreg2  27498  xrge00  30020  submatres  30206  madjusmdetlem2  30228  madjusmdetlem3  30229  qtophaus  30237  fsumcvg4  30330  gsumesum  30455  pwsiga  30527  sigainb  30533  carsggect  30714  omsmeas  30719  sitgclg  30738  ballotlemfelz  30886  ballotlemfp1  30887  ballotth  30933  cxpcncf1  31007  logdivsqrle  31062  hgt750lemb  31068  kur14lem6  31525  kur14lem7  31526  cvmscld  31587  mclsppslem  31812  fundmpss  31996  frpoind  32071  frind  32074  relsset  32326  limitssson  32349  fnsingle  32357  funimage  32366  cldbnd  32652  clsun  32654  topdifinffinlem  33525  matunitlindflem1  33731  poimirlem8  33743  poimirlem26  33761  poimirlem30  33765  mblfinlem3  33774  mblfinlem4  33775  ismblfin  33776  voliunnfl  33779  cnambfre  33783  dvtan  33785  dvasin  33821  dvacos  33822  areacirclem4  33828  fdc  33866  divrngcl  34081  isdrngo2  34082  isdrngo3  34083  islsati  34796  hdmap14lem2a  37670  istopclsd  37782  diophin  37855  dnnumch1  38133  cntzsdrg  38291  isdomn3  38301  deg1mhm  38304  gneispace  38951  sumnnodd  40374  cncficcgt0  40613  cncfiooicclem1  40618  cxpcncf2  40625  dirkercncflem2  40832  fourierdlem62  40896  fourierdlem66  40900  fourierdlem68  40902  fourierdlem95  40929  etransclem24  40986  etransclem44  41006  gsumge0cl  41099  sge0fodjrnlem  41144  carageniuncllem1  41249  smfresal  41509  lindslinindimp2lem2  42766  amgmlemALT  43070
  Copyright terms: Public domain W3C validator