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

Definition df-ss 3367
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, (ex-ss 22244). Note that (proved in ssid 3400). Contrast this relationship with the relationship (as will be defined in df-pss 3369). For a more traditional definition, but requiring a dummy variable, see dfss2 3370. Other possible definitions are given by dfss3 3371, dfss4 3607, sspss 3479, ssequn1 3550, ssequn2 3553, sseqin2 3592, and ssdif0 3759. (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
df-ss

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wss 3353 . 2
41, 2cin 3352 . . 3
54, 1wceq 1662 . 2
63, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  dfss  3368  dfss1  3578  inabs  3604  nssinpss  3605  dfrab3ss  3651  disjssun  3758  riinn0  4255  rintn0  4271  ssex  4446  op1stb  4569  ordtri3or  4754  ssdmres  5137  resima2  5148  xpssres  5149  fnimaeq0  5529  fnreseql  5802  sorpssin  6334  curry1  6621  curry2  6624  tpostpos2  6683  tz7.44-2  6777  tz7.44-3  6778  frfnom  6804  ecinxp  7091  infssuni  7509  elfiun  7547  marypha1lem  7550  unxpwdom  7669  cdainf  8186  ackbij1lem16  8229  fin23lem26  8319  isf34lem7  8373  isf34lem6  8374  fpwwe2lem11  8629  fpwwe2lem13  8631  fpwwe2  8632  uzin  10700  iooval2  11140  limsupgle  12741  limsupgre  12745  bitsinv1  13424  bitsres  13455  bitsuz  13456  2prm  13565  dfphi2  13635  ressbas2  14011  ressinbas  14016  ressress  14017  restid2  14149  resscatc  14751  dprdz  16091  dprdcntz2  16099  lmhmlsp  16628  lspdisj2  16702  ressmplbas2  17021  difopn  17601  mretopd  17659  restcld  17739  restopnb  17742  restfpw  17746  neitr  17747  cnrest2  17853  paste  17861  isnrm2  17925  1stccnp  18029  restnlly  18049  lly1stc  18063  kgeni  18073  kgencn3  18094  ptbasfi  18117  hausdiag  18181  qtopval2  18232  qtoprest  18253  filcon  18419  trfil2  18423  trfg  18427  uzrest  18433  trufil  18446  ufileu  18455  fclscf  18561  flimfnfcls  18564  tsmsres  18677  trust  18763  restutopopn  18772  metustfbasOLD  19099  metustfbas  19100  restmetu  19121  xrtgioo  19341  xrsmopn  19347  clsocv  19708  cmetss  19771  ovoliunlem1  19902  difmbl  19941  voliunlem1  19948  volsup2  20001  i1fima  20072  i1fima2  20073  i1fd  20075  itg1addlem5  20094  itg1climres  20108  dvmptid  20347  dvmptc  20348  dvlipcn  20382  dvlip2  20383  dvcnvrelem1  20405  dvcvx  20408  taylthlem1  20793  taylthlem2  20794  psercn  20846  pige3  20934  dvlog  21051  dvcxp1  21135  ppiprm  21443  chtprm  21445  eupares  22206  chm1i  23469  dmdsl3  24329  atssma  24392  dmdbr6ati  24437  imadifxp  24558  fnresin  24566  sspreima  24583  df1stres  24620  df2ndres  24621  xrge0base  24768  xrge00  24769  xrge0slmod  24982  esumnul  25173  esumsn  25186  eulerpartlemgs2  25428  probmeasb  25454  ballotlemfp1  25515  signstres  25618  cvmscld  25799  cvmliftmolem1  25807  dfon2lem4  26243  dfrdg2  26253  sspred  26277  nodense  26474  fvline2  26910  mblfinlem3  27101  mblfinlem4  27102  ftc1anclem6  27143  areacirclem1  27155  topbnd  27190  opnbnd  27191  neibastop1  27251  subspopn  27321  ssbnd  27360  heiborlem3  27385  elrfi  27679  setindtr  28024  fnwe2lem2  28055  lmhmlnmsplit  28091  pmtrmvd  28304  proot1hash  28425  fgraphopab  28435  dmressnsn  28884  fnresfnco  28888  resisresindm  28997  f0rn0  29000  bnj1322  30387  lcvexchlem3  31107  dihglblem5aN  33363
  Copyright terms: Public domain W3C validator