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

Theorem difss 4062
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 4057 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3922 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cdif 3881  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-dif 3887  df-in 3891  df-ss 3901
This theorem is referenced by:  difssd  4063  difss2  4064  ssdifss  4066  0dif  4312  disj4  4369  difsnpss  4703  unidif  4837  iunxdif2  4943  difexg  5198  difelpw  5220  reldif  5656  cnvdif  5973  difxp  5992  wfi  6153  tz7.7  6189  fresaun  6527  fresaunres2  6528  resdif  6614  fndmdif  6793  tfi  7552  peano5  7589  wfrlem16  7957  oelim2  8208  swoer  8306  swoord1  8307  swoord2  8308  ralxpmap  8447  boxcutc  8492  undom  8592  domunsncan  8604  sbthlem2  8616  sbthlem4  8618  sbthlem5  8619  limenpsi  8680  phplem2  8685  php3  8691  diffi  8738  frfi  8751  fofinf1o  8787  ixpfi2  8810  elfiun  8882  marypha1lem  8885  wemapso  9003  infdifsn  9108  cantnflem2  9141  dfac8alem  9444  acnnum  9467  inffien  9478  kmlem5  9569  infdif  9624  infdif2  9625  ackbij1lem18  9652  fictb  9660  fin23lem7  9731  fin23lem11  9732  fin23lem28  9755  fin23lem30  9757  compsscnvlem  9785  isf34lem2  9788  compssiso  9789  isf34lem4  9792  fin1a2lem7  9821  axcclem  9872  zornn0g  9920  ttukey2g  9931  pinn  10293  niex  10296  ltsopi  10303  dmaddpi  10305  dmmulpi  10306  lerelxr  10697  mulnzcnopr  11279  dflt2  12533  expcl2lem  13441  expclzlem  13453  hashun2  13744  fsumss  15077  fsumless  15146  cvgcmpce  15168  fprodss  15297  rpnnen2lem9  15570  isstruct2  16488  structcnvcnv  16492  fsets  16511  strleun  16586  strle1  16587  mreexexlem2d  16911  gsumpropd2lem  17884  symgfixf1  18560  f1omvdmvd  18566  mvdco  18568  f1omvdconj  18569  pmtrfb  18588  pmtrfconj  18589  symggen  18593  symggen2  18594  psgnunilem1  18616  frgpnabllem2  18990  dprdss  19147  dprd2da  19160  dmdprdsplit2lem  19163  dpjidcl  19176  ablfac1b  19188  ablfac1eu  19191  isdrng2  19508  drngmcl  19511  drngid2  19514  isdrngd  19523  cntzsdrg  19577  subdrgint  19578  xrs1mnd  20132  xrs10  20133  xrs1cmn  20134  xrge0subm  20135  xrge0cmn  20136  cnmgpid  20156  cnmsubglem  20157  expghm  20192  dsmmfi  20430  islinds2  20505  lindsind2  20511  lindfrn  20513  islindf4  20530  mdetdiaglem  21206  mdetrsca2  21212  mdetrlin2  21215  mdetralt  21216  mdetunilem5  21224  mdetunilem9  21228  maducoeval2  21248  smadiadetglem1  21279  isopn2  21640  ntrval2  21659  ntrdif  21660  clsdif  21661  ntrss  21663  cmclsopn  21670  discld  21697  mretopd  21700  lpsscls  21749  restntr  21790  cmpcld  22010  2ndcsep  22067  1stccnp  22070  llycmpkgen2  22158  1stckgen  22162  txkgen  22260  qtopcld  22321  qtopcmap  22327  kqdisj  22340  isufil2  22516  ufileu  22527  filufint  22528  fixufil  22530  cfinufil  22536  ufilen  22538  fin1aufil  22540  supnfcls  22628  flimfnfcls  22636  alexsublem  22652  alexsubALTlem3  22657  cldsubg  22719  imasdsf1olem  22983  recld2  23422  sszcld  23425  xrge0gsumle  23441  divcn  23476  cdivcncf  23529  bcth3  23938  ismbl2  24134  cmmbl  24141  nulmbl  24142  nulmbl2  24143  unmbl  24144  voliunlem1  24157  voliunlem2  24158  ioombl1lem4  24168  ioombl1  24169  uniioombllem3  24192  mbfss  24253  itg1cl  24292  itg1ge0  24293  i1f0  24294  i1f1  24297  i1fmul  24303  itg1addlem4  24306  itg1mulc  24311  itg10a  24317  itg1ge0a  24318  itg1climres  24321  itg2cnlem1  24368  itgioo  24422  itgsplitioo  24444  limcdif  24482  ellimc2  24483  ellimc3  24485  limcflflem  24486  limcflf  24487  limcmo  24488  limcresi  24491  dvreslem  24515  dvres2lem  24516  dvidlem  24521  dvcnp2  24526  dvaddbr  24544  dvmulbr  24545  dvcobr  24552  dvrec  24561  dvcnvlem  24582  lhop1lem  24619  lhop  24622  tdeglem4  24664  deg1n0ima  24693  aacjcl  24926  taylthlem2  24972  abelth  25039  logcnlem5  25240  dvlog2  25247  efopnlem2  25251  dvcncxp1  25335  dvcnsqrt  25336  cxpcn2  25338  sqrtcn  25342  efrlim  25558  jensen  25577  amgm  25579  lgamgulmlem2  25618  lgamucov  25626  wilthlem2  25657  dchrelbas2  25824  rpvmasum2  26099  dchrisum0re  26100  dchrisum0lem3  26106  dchrisum0  26107  tgisline  26424  upgrss  26884  frgrwopreg2  28107  difxp1ss  30297  difxp2ss  30298  xrge00  30723  symgcom2  30781  pmtrcnel  30786  pmtrcnel2  30787  pmtrcnelor  30788  cycpmrn  30838  tocyccntz  30839  submatres  31159  madjusmdetlem2  31181  madjusmdetlem3  31182  qtophaus  31189  fsumcvg4  31301  gsumesum  31426  pwsiga  31497  sigainb  31503  carsggect  31684  omsmeas  31689  sitgclg  31708  ballotlemfelz  31856  ballotlemfp1  31857  ballotth  31903  cxpcncf1  31974  logdivsqrle  32029  hgt750lemb  32035  kur14lem6  32566  kur14lem7  32567  cvmscld  32628  satfvsucsuc  32720  satfrnmapom  32725  mclsppslem  32938  fundmpss  33117  frpoind  33188  frind  33193  frr1  33252  relsset  33457  limitssson  33480  fnsingle  33488  funimage  33497  cldbnd  33782  clsun  33784  topdifinffinlem  34759  inunissunidif  34787  pibt2  34829  matunitlindflem1  35046  poimirlem8  35058  poimirlem26  35076  poimirlem30  35080  mblfinlem3  35089  mblfinlem4  35090  ismblfin  35091  voliunnfl  35094  cnambfre  35098  dvtan  35100  dvasin  35134  dvacos  35135  areacirclem4  35141  fdc  35176  divrngcl  35388  isdrngo2  35389  isdrngo3  35390  islsati  36283  hdmap14lem2a  39156  prjspreln0  39590  prjspvs  39591  prjspeclsp  39593  0prjspnrel  39600  istopclsd  39628  diophin  39700  dnnumch1  39975  isdomn3  40135  deg1mhm  40138  gneispace  40824  inaex  40992  sumnnodd  42259  cncficcgt0  42517  cncfiooicclem1  42522  cxpcncf2  42528  dirkercncflem2  42733  fourierdlem62  42797  fourierdlem66  42801  fourierdlem68  42803  fourierdlem95  42830  etransclem24  42887  etransclem44  42907  gsumge0cl  42997  sge0fodjrnlem  43042  carageniuncllem1  43147  smfresal  43407  lindslinindimp2lem2  44855  amgmlemALT  45318
  Copyright terms: Public domain W3C validator