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

Theorem difss 3720
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 3715 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3591 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cdif 3556  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-dif 3562  df-in 3566  df-ss 3573
This theorem is referenced by:  difssd  3721  difss2  3722  ssdifss  3724  0dif  3954  disj4  4002  uneqdifeqOLD  4035  difsnpss  4312  unidif  4442  iunxdif2  4539  difexg  4773  reldif  5204  cnvdif  5503  difxp  5522  wfi  5677  tz7.7  5713  fresaun  6037  fresaunres2  6038  resdif  6119  fndmdif  6282  tfi  7007  peano5  7043  wfrlem16  7382  oev  7546  oelim2  7627  swoer  7724  swoord1  7725  swoord2  7726  ralxpmap  7859  boxcutc  7903  undom  8000  domunsncan  8012  sbthlem2  8023  sbthlem4  8025  sbthlem5  8026  limenpsi  8087  phplem2  8092  php  8096  php3  8098  pssnn  8130  diffi  8144  frfi  8157  fofinf1o  8193  ixpfi2  8216  elfiun  8288  marypha1lem  8291  wemapso  8408  infdifsn  8506  cantnflem2  8539  dfac8alem  8804  acnnum  8827  inffien  8838  kmlem5  8928  infdif  8983  infdif2  8984  ackbij1lem18  9011  fictb  9019  fin23lem7  9090  fin23lem11  9091  fin23lem28  9114  fin23lem30  9116  compsscnvlem  9144  isf34lem2  9147  compssiso  9148  isf34lem4  9151  fin1a2lem7  9180  domtriomlem  9216  axcclem  9231  zornn0g  9279  ttukey2g  9290  konigthlem  9342  pinn  9652  niex  9655  ltsopi  9662  dmaddpi  9664  dmmulpi  9665  lerelxr  10053  mulnzcnopr  10625  dflt2  11933  expcl2lem  12820  expclzlem  12832  hashun2  13120  fsumss  14397  fsumless  14466  cvgcmpce  14488  fprodss  14614  rpnnen2lem9  14887  isstruct2  15801  structcnvcnv  15805  fsets  15823  strleun  15904  strle1  15905  mreexexlem2d  16237  gsumpropd2lem  17205  symgfixf1  17789  f1omvdmvd  17795  mvdco  17797  f1omvdconj  17798  pmtrfb  17817  pmtrfconj  17818  symggen  17822  symggen2  17823  psgnunilem1  17845  frgpnabllem2  18209  dprdss  18360  dprd2da  18373  dmdprdsplit2lem  18376  dpjidcl  18389  ablfac1b  18401  ablfac1eu  18404  isdrng2  18689  drngmcl  18692  drngid2  18695  isdrngd  18704  xrs1mnd  19716  xrs10  19717  xrs1cmn  19718  xrge0subm  19719  xrge0cmn  19720  cnmgpid  19740  cnmsubglem  19741  expghm  19776  cnmsgngrp  19857  psgninv  19860  dsmmfi  20014  islinds2  20084  lindsind2  20090  lindfrn  20092  islindf4  20109  mdetdiaglem  20336  mdetrsca2  20342  mdetrlin2  20345  mdetralt  20346  mdetunilem5  20354  mdetunilem9  20358  maducoeval2  20378  smadiadetglem1  20409  isopn2  20759  ntrval2  20778  ntrdif  20779  clsdif  20780  ntrss  20782  cmclsopn  20789  discld  20816  mretopd  20819  lpsscls  20868  restntr  20909  cmpcld  21128  2ndcsep  21185  1stccnp  21188  llycmpkgen2  21276  1stckgen  21280  txkgen  21378  qtopcld  21439  qtopcmap  21445  kqdisj  21458  isufil2  21635  ufileu  21646  filufint  21647  fixufil  21649  cfinufil  21655  ufilen  21657  fin1aufil  21659  supnfcls  21747  flimfnfcls  21755  alexsublem  21771  alexsubALTlem3  21776  cldsubg  21837  imasdsf1olem  22101  recld2  22540  sszcld  22543  xrge0gsumle  22559  divcn  22594  cdivcncf  22643  bcth3  23051  ismbl2  23218  cmmbl  23225  nulmbl  23226  nulmbl2  23227  unmbl  23228  voliunlem1  23241  voliunlem2  23242  ioombl1lem4  23252  ioombl1  23253  uniioombllem3  23276  mbfss  23336  itg1cl  23375  itg1ge0  23376  i1f0  23377  i1f1  23380  i1fmul  23386  itg1addlem4  23389  itg1mulc  23394  itg10a  23400  itg1ge0a  23401  itg1climres  23404  itg2cnlem1  23451  itgioo  23505  itgsplitioo  23527  limcdif  23563  ellimc2  23564  ellimc3  23566  limcflflem  23567  limcflf  23568  limcmo  23569  limcresi  23572  dvreslem  23596  dvres2lem  23597  dvidlem  23602  dvcnp2  23606  dvaddbr  23624  dvmulbr  23625  dvcobr  23632  dvrec  23641  dvcnvlem  23660  lhop1lem  23697  lhop  23700  tdeglem4  23741  deg1n0ima  23770  aacjcl  24003  taylthlem2  24049  abelth  24116  logcnlem5  24309  dvlog2  24316  efopnlem2  24320  dvcncxp1  24401  dvcnsqrt  24402  cxpcn2  24404  sqrtcn  24408  efrlim  24613  jensen  24632  amgm  24634  lgamgulmlem2  24673  lgamucov  24681  wilthlem2  24712  dchrelbas2  24879  rpvmasum2  25118  dchrisum0re  25119  dchrisum0lem3  25125  dchrisum0  25126  tgisline  25439  upgrss  25896  frgrwopreg2  27063  xrge00  29495  submatres  29678  madjusmdetlem2  29700  madjusmdetlem3  29701  qtophaus  29709  fsumcvg4  29802  gsumesum  29926  pwsiga  29998  sigainb  30004  carsggect  30185  omsmeas  30190  sitgclg  30209  ballotlemfelz  30357  ballotlemfp1  30358  ballotth  30404  kur14lem6  30936  kur14lem7  30937  cvmscld  30998  mclsppslem  31223  fundmpss  31403  frind  31476  relsset  31672  limitssson  31695  fnsingle  31703  funimage  31712  cldbnd  31998  clsun  32000  topdifinffinlem  32862  matunitlindflem1  33072  poimirlem8  33084  poimirlem26  33102  poimirlem30  33106  mblfinlem3  33115  mblfinlem4  33116  ismblfin  33117  voliunnfl  33120  cnambfre  33125  dvtan  33127  dvasin  33163  dvacos  33164  areacirclem4  33170  fdc  33208  divrngcl  33423  isdrngo2  33424  isdrngo3  33425  islsati  33796  hdmap14lem2a  36674  istopclsd  36778  diophin  36851  dnnumch1  37129  cntzsdrg  37288  isdomn3  37298  deg1mhm  37301  gneispace  37949  sumnnodd  39294  cncficcgt0  39432  cncfiooicclem1  39437  cxpcncf2  39444  dirkercncflem2  39654  fourierdlem62  39718  fourierdlem66  39722  fourierdlem68  39724  fourierdlem95  39751  etransclem24  39808  etransclem44  39828  gsumge0cl  39921  sge0fodjrnlem  39966  carageniuncllem1  40068  smfresal  40328  lindslinindimp2lem2  41562  amgmlemALT  41878
  Copyright terms: Public domain W3C validator