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

Definition df-ss 3489
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, (ex-ss 25148). Note that (proved in ssid 3522). Contrast this relationship with the relationship (as will be defined in df-pss 3491). For a more traditional definition, but requiring a dummy variable, see dfss2 3492. Other possible definitions are given by dfss3 3493, dfss4 3731, sspss 3602, ssequn1 3673, ssequn2 3676, sseqin2 3716, and ssdif0 3885. (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 3475 . 2
41, 2cin 3474 . . 3
54, 1wceq 1395 . 2
63, 5wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3490  dfss1  3702  inabs  3728  nssinpss  3729  dfrab3ss  3775  disjssun  3884  riinn0  4405  rintn0  4421  ssex  4596  op1stb  4722  ordtri3or  4915  ssdmres  5300  resima2  5312  xpssres  5313  dmressnsn  5317  fnimaeq0  5707  f0rn0  5775  fnreseql  5997  sorpssin  6588  curry1  6892  curry2  6895  tpostpos2  6995  tz7.44-2  7092  tz7.44-3  7093  frfnom  7119  ecinxp  7405  infssuni  7831  elfiun  7910  marypha1lem  7913  unxpwdom  8036  cdainf  8593  ackbij1lem16  8636  fin23lem26  8726  isf34lem7  8780  isf34lem6  8781  fpwwe2lem11  9039  fpwwe2lem13  9041  fpwwe2  9042  uzin  11142  iooval2  11591  limsupgle  13300  limsupgre  13304  bitsinv1  14092  bitsres  14123  bitsuz  14124  2prm  14233  dfphi2  14304  ressbas2  14688  ressinbas  14693  ressress  14694  restid2  14828  resscatc  15432  pmtrmvd  16481  dprdz  17077  dprdcntz2  17086  lmhmlsp  17695  lspdisj2  17773  ressmplbas2  18117  difopn  19535  mretopd  19593  restcld  19673  restopnb  19676  restfpw  19680  neitr  19681  cnrest2  19787  paste  19795  isnrm2  19859  1stccnp  19963  restnlly  19983  lly1stc  19997  kgeni  20038  kgencn3  20059  ptbasfi  20082  hausdiag  20146  qtopval2  20197  qtoprest  20218  filcon  20384  trfil2  20388  trfg  20392  uzrest  20398  trufil  20411  ufileu  20420  fclscf  20526  flimfnfcls  20529  tsmsresOLD  20645  tsmsres  20646  trust  20732  restutopopn  20741  metustfbasOLD  21068  metustfbas  21069  restmetu  21090  xrtgioo  21311  xrsmopn  21317  clsocv  21690  cmetss  21753  ovoliunlem1  21913  difmbl  21953  voliunlem1  21960  volsup2  22014  i1fima  22085  i1fima2  22086  i1fd  22088  itg1addlem5  22107  itg1climres  22121  dvmptid  22360  dvmptc  22361  dvlipcn  22395  dvlip2  22396  dvcnvrelem1  22418  dvcvx  22421  taylthlem1  22768  taylthlem2  22769  psercn  22821  pige3  22910  dvlog  23032  dvcxp1  23116  ppiprm  23425  chtprm  23427  eupares  24975  chm1i  26374  dmdsl3  27234  atssma  27297  dmdbr6ati  27342  imadifxp  27458  fnresin  27470  sspreima  27485  df1stres  27522  df2ndres  27523  xrge0base  27673  xrge00  27674  xrge0slmod  27834  esumnul  28059  esumsn  28072  eulerpartlemgs2  28319  probmeasb  28369  ballotlemfp1  28430  signstres  28532  cvmscld  28718  cvmliftmolem1  28726  mrsubvrs  28882  elmsta  28908  dfon2lem4  29218  dfrdg2  29228  sspred  29252  nodense  29449  fvline2  29796  mblfinlem3  30053  mblfinlem4  30054  ftc1anclem6  30095  areacirclem1  30107  topbnd  30142  opnbnd  30143  neibastop1  30177  subspopn  30245  ssbnd  30284  heiborlem3  30309  elrfi  30626  setindtr  30966  fnwe2lem2  30997  lmhmlnmsplit  31033  proot1hash  31160  fgraphopab  31170  fouriersw  32014  fnresfnco  32211  resisresindm  32305  ressval3d  32558  lidlbas  32729  bnj1322  33881  lcvexchlem3  34761  dihglblem5aN  37019
  Copyright terms: Public domain W3C validator