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

Theorem difss 3735
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 3730 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3605 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cdif 3569  wss 3572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-dif 3575  df-in 3579  df-ss 3586
This theorem is referenced by:  difssd  3736  difss2  3737  ssdifss  3739  0dif  3975  disj4  4023  uneqdifeqOLD  4056  difsnpss  4336  unidif  4469  iunxdif2  4566  difexg  4806  reldif  5236  cnvdif  5537  difxp  5556  wfi  5711  tz7.7  5747  fresaun  6073  fresaunres2  6074  resdif  6155  fndmdif  6319  tfi  7050  peano5  7086  wfrlem16  7427  oev  7591  oelim2  7672  swoer  7769  swoord1  7770  swoord2  7771  ralxpmap  7904  boxcutc  7948  undom  8045  domunsncan  8057  sbthlem2  8068  sbthlem4  8070  sbthlem5  8071  limenpsi  8132  phplem2  8137  php  8141  php3  8143  pssnn  8175  diffi  8189  frfi  8202  fofinf1o  8238  ixpfi2  8261  elfiun  8333  marypha1lem  8336  wemapso  8453  infdifsn  8551  cantnflem2  8584  dfac8alem  8849  acnnum  8872  inffien  8883  kmlem5  8973  infdif  9028  infdif2  9029  ackbij1lem18  9056  fictb  9064  fin23lem7  9135  fin23lem11  9136  fin23lem28  9159  fin23lem30  9161  compsscnvlem  9189  isf34lem2  9192  compssiso  9193  isf34lem4  9196  fin1a2lem7  9225  domtriomlem  9261  axcclem  9276  zornn0g  9324  ttukey2g  9335  konigthlem  9387  pinn  9697  niex  9700  ltsopi  9707  dmaddpi  9709  dmmulpi  9710  lerelxr  10098  mulnzcnopr  10670  dflt2  11978  expcl2lem  12867  expclzlem  12879  hashun2  13167  fsumss  14450  fsumless  14522  cvgcmpce  14544  fprodss  14672  rpnnen2lem9  14945  isstruct2  15861  structcnvcnv  15865  fsets  15885  strleun  15966  strle1  15967  mreexexlem2d  16299  gsumpropd2lem  17267  symgfixf1  17851  f1omvdmvd  17857  mvdco  17859  f1omvdconj  17860  pmtrfb  17879  pmtrfconj  17880  symggen  17884  symggen2  17885  psgnunilem1  17907  frgpnabllem2  18271  dprdss  18422  dprd2da  18435  dmdprdsplit2lem  18438  dpjidcl  18451  ablfac1b  18463  ablfac1eu  18466  isdrng2  18751  drngmcl  18754  drngid2  18757  isdrngd  18766  xrs1mnd  19778  xrs10  19779  xrs1cmn  19780  xrge0subm  19781  xrge0cmn  19782  cnmgpid  19802  cnmsubglem  19803  expghm  19838  cnmsgngrp  19919  psgninv  19922  dsmmfi  20076  islinds2  20146  lindsind2  20152  lindfrn  20154  islindf4  20171  mdetdiaglem  20398  mdetrsca2  20404  mdetrlin2  20407  mdetralt  20408  mdetunilem5  20416  mdetunilem9  20420  maducoeval2  20440  smadiadetglem1  20471  isopn2  20830  ntrval2  20849  ntrdif  20850  clsdif  20851  ntrss  20853  cmclsopn  20860  discld  20887  mretopd  20890  lpsscls  20939  restntr  20980  cmpcld  21199  2ndcsep  21256  1stccnp  21259  llycmpkgen2  21347  1stckgen  21351  txkgen  21449  qtopcld  21510  qtopcmap  21516  kqdisj  21529  isufil2  21706  ufileu  21717  filufint  21718  fixufil  21720  cfinufil  21726  ufilen  21728  fin1aufil  21730  supnfcls  21818  flimfnfcls  21826  alexsublem  21842  alexsubALTlem3  21847  cldsubg  21908  imasdsf1olem  22172  recld2  22611  sszcld  22614  xrge0gsumle  22630  divcn  22665  cdivcncf  22714  bcth3  23122  ismbl2  23289  cmmbl  23296  nulmbl  23297  nulmbl2  23298  unmbl  23299  voliunlem1  23312  voliunlem2  23313  ioombl1lem4  23323  ioombl1  23324  uniioombllem3  23347  mbfss  23407  itg1cl  23446  itg1ge0  23447  i1f0  23448  i1f1  23451  i1fmul  23457  itg1addlem4  23460  itg1mulc  23465  itg10a  23471  itg1ge0a  23472  itg1climres  23475  itg2cnlem1  23522  itgioo  23576  itgsplitioo  23598  limcdif  23634  ellimc2  23635  ellimc3  23637  limcflflem  23638  limcflf  23639  limcmo  23640  limcresi  23643  dvreslem  23667  dvres2lem  23668  dvidlem  23673  dvcnp2  23677  dvaddbr  23695  dvmulbr  23696  dvcobr  23703  dvrec  23712  dvcnvlem  23733  lhop1lem  23770  lhop  23773  tdeglem4  23814  deg1n0ima  23843  aacjcl  24076  taylthlem2  24122  abelth  24189  logcnlem5  24386  dvlog2  24393  efopnlem2  24397  dvcncxp1  24478  dvcnsqrt  24479  cxpcn2  24481  sqrtcn  24485  efrlim  24690  jensen  24709  amgm  24711  lgamgulmlem2  24750  lgamucov  24758  wilthlem2  24789  dchrelbas2  24956  rpvmasum2  25195  dchrisum0re  25196  dchrisum0lem3  25202  dchrisum0  25203  tgisline  25516  upgrss  25977  frgrwopreg2  27174  xrge00  29671  submatres  29857  madjusmdetlem2  29879  madjusmdetlem3  29880  qtophaus  29888  fsumcvg4  29981  gsumesum  30106  pwsiga  30178  sigainb  30184  carsggect  30365  omsmeas  30370  sitgclg  30389  ballotlemfelz  30537  ballotlemfp1  30538  ballotth  30584  cxpcncf1  30658  logdivsqrle  30713  hgt750lemb  30719  kur14lem6  31178  kur14lem7  31179  cvmscld  31240  mclsppslem  31465  fundmpss  31650  frind  31724  relsset  31979  limitssson  32002  fnsingle  32010  funimage  32019  cldbnd  32305  clsun  32307  topdifinffinlem  33175  matunitlindflem1  33385  poimirlem8  33397  poimirlem26  33415  poimirlem30  33419  mblfinlem3  33428  mblfinlem4  33429  ismblfin  33430  voliunnfl  33433  cnambfre  33438  dvtan  33440  dvasin  33476  dvacos  33477  areacirclem4  33483  fdc  33521  divrngcl  33736  isdrngo2  33737  isdrngo3  33738  islsati  34107  hdmap14lem2a  36985  istopclsd  37089  diophin  37162  dnnumch1  37440  cntzsdrg  37598  isdomn3  37608  deg1mhm  37611  gneispace  38258  sumnnodd  39668  cncficcgt0  39870  cncfiooicclem1  39875  cxpcncf2  39882  dirkercncflem2  40090  fourierdlem62  40154  fourierdlem66  40158  fourierdlem68  40160  fourierdlem95  40187  etransclem24  40244  etransclem44  40264  gsumge0cl  40357  sge0fodjrnlem  40402  carageniuncllem1  40504  smfresal  40764  lindslinindimp2lem2  42019  amgmlemALT  42320
  Copyright terms: Public domain W3C validator