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

Theorem difss 3630
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 3625 . 2
21ssriv 3507 1
Colors of variables: wff setvar class
Syntax hints:  \cdif 3472  C_wss 3475
This theorem is referenced by:  difssd  3631  difss2  3632  ssdifss  3634  disj4  3875  0dif  3899  uneqdifeq  3916  difsnpss  4173  unidif  4283  iunxdif2  4378  difexg  4600  tz7.7  4909  reldif  5127  cnvdif  5417  difxp  5436  fresaun  5761  fresaunres2  5762  resdif  5841  fndmdif  5991  tfi  6688  peano5  6723  oev  7183  oelim2  7263  swoer  7358  swoord1  7359  swoord2  7360  ralxpmap  7488  boxcutc  7532  undom  7625  domunsncan  7637  sbthlem2  7648  sbthlem4  7650  sbthlem5  7651  limenpsi  7712  phplem2  7717  php  7721  php3  7723  pssnn  7758  diffi  7771  frfi  7785  fofinf1o  7821  ixpfi2  7838  elfiun  7910  marypha1lem  7913  wemapso  7997  inf3lem3  8068  infdifsn  8094  cantnflem2  8130  dfac8alem  8431  acnnum  8454  inffien  8465  kmlem5  8555  infdif  8610  infdif2  8611  ackbij1lem18  8638  fictb  8646  fin23lem7  8717  fin23lem11  8718  fin23lem28  8741  fin23lem30  8743  compsscnvlem  8771  isf34lem2  8774  compssiso  8775  isf34lem4  8778  fin1a2lem7  8807  domtriomlem  8843  axcclem  8858  zornn0g  8906  ttukey2g  8917  konigthlem  8964  pinn  9277  niex  9280  ltsopi  9287  dmaddpi  9289  dmmulpi  9290  lerelxr  9671  mulnzcnopr  10220  dflt2  11383  expcl2lem  12178  expclzlem  12190  hashun2  12451  fsumss  13547  fsumless  13610  cvgcmpce  13632  fprodss  13755  rpnnen2lem9  13956  isstruct2  14641  structcnvcnv  14643  fsets  14658  strleun  14727  strle1  14728  mreexexlem2d  15042  gsumpropd2lem  15900  symgfixf1  16462  f1omvdmvd  16468  mvdco  16470  f1omvdconj  16471  pmtrfb  16490  pmtrfconj  16491  symggen  16495  symggen2  16496  psgnunilem1  16518  frgpnabllem2  16878  dprdss  17076  dprd2da  17091  dmdprdsplit2lem  17094  dpjidcl  17107  dpjidclOLD  17114  ablfac1b  17121  ablfac1eu  17124  isdrng2  17406  drngmcl  17409  drngid2  17412  isdrngd  17421  xrs1mnd  18456  xrs10  18457  xrs1cmn  18458  xrge0subm  18459  xrge0cmn  18460  cnmsubglem  18480  expghm  18529  expghmOLD  18530  cnmsgngrp  18615  psgninv  18618  dsmmfi  18769  islinds2  18848  lindsind2  18854  lindfrn  18856  islindf4  18873  mdetdiaglem  19100  mdetrsca2  19106  mdetrlin2  19109  mdetralt  19110  mdetunilem5  19118  mdetunilem9  19122  maducoeval2  19142  smadiadetglem1  19173  isopn2  19533  ntrval2  19552  ntrdif  19553  clsdif  19554  ntrss  19556  cmclsopn  19563  cmntrcld  19564  discld  19590  mretopd  19593  lpsscls  19642  restntr  19683  cmpcld  19902  2ndcsep  19960  1stccnp  19963  llycmpkgen2  20051  1stckgen  20055  txkgen  20153  qtopcld  20214  qtopcmap  20220  kqdisj  20233  isufil2  20409  ufileu  20420  filufint  20421  fixufil  20423  cfinufil  20429  ufilen  20431  fin1aufil  20433  supnfcls  20521  flimfnfcls  20529  alexsublem  20544  alexsubALTlem3  20549  cldsubg  20609  imasdsf1olem  20876  recld2  21319  sszcld  21322  xrge0gsumle  21338  divcn  21372  cdivcncf  21421  bcth3  21770  ismbl2  21938  cmmbl  21945  nulmbl  21946  nulmbl2  21947  unmbl  21948  voliunlem1  21960  voliunlem2  21961  ioombl1lem4  21971  ioombl1  21972  uniioombllem3  21994  mbfss  22053  itg1cl  22092  itg1ge0  22093  i1f0  22094  i1f1  22097  i1fmul  22103  itg1addlem4  22106  itg1mulc  22111  itg10a  22117  itg1ge0a  22118  itg1climres  22121  itg2cnlem1  22168  itgioo  22222  itgsplitioo  22244  limcdif  22280  ellimc2  22281  ellimc3  22283  limcflflem  22284  limcflf  22285  limcmo  22286  limcresi  22289  dvreslem  22313  dvres2lem  22314  dvidlem  22319  dvcnp2  22323  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvrec  22358  dvcnvlem  22377  lhop1lem  22414  lhop  22417  tdeglem4  22458  deg1n0ima  22489  aacjcl  22723  taylthlem2  22769  abelth  22836  logcnlem5  23027  dvlog2  23034  efopnlem2  23038  cxpcn2  23120  sqrtcn  23124  efrlim  23299  jensen  23318  amgm  23320  wilthlem2  23343  dchrelbas2  23512  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lem3  23704  dchrisum0  23705  tgisline  24007  umgrass  24319  frgrawopreg2  25051  xrge00  27674  qtophaus  27839  fsumcvg4  27932  gsumesum  28067  pwsiga  28130  sigainb  28136  sitgclg  28284  ballotlemfelz  28429  ballotlemfp1  28430  ballotth  28476  lgamgulmlem2  28572  lgamucov  28580  kur14lem6  28655  kur14lem7  28656  cvmscld  28718  mclsppslem  28943  fundmpss  29196  wfi  29287  frind  29323  wfrlem16  29358  relsset  29538  limitssson  29561  fnsingle  29569  funimage  29578  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  voliunnfl  30058  cnambfre  30063  dvtan  30065  dvcncxp1  30100  dvcnsqrt  30101  dvasin  30103  dvacos  30104  areacirclem4  30110  cldbnd  30144  clsun  30146  fdc  30238  divrngcl  30360  isdrngo2  30361  isdrngo3  30362  istopclsd  30632  diophin  30706  setindtr  30966  dnnumch1  30990  cntzsdrg  31151  isdomn3  31164  deg1mhm  31167  sumnnodd  31636  cncficcgt0  31691  cncfiooicclem1  31696  cxpcncf2  31703  dirkercncflem2  31886  fourierdlem62  31951  fourierdlem66  31955  fourierdlem68  31957  fourierdlem95  31984  etransclem24  32041  etransclem44  32061  lindslinindimp2lem2  33060  islsati  34719  hdmap14lem2a  37597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator