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

Definition df-ss 3323
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. ?Error: 1 , 2 } C_ { 1 , 2 , 3 } ^ This math symbol is not active (i.e. was not declared in this scope). For example, {1,2}C_{1,2,3} (ex-ss 21786). Note that (proved in ssid 3356). Contrast this relationship with the relationship (as will be defined in df-pss 3325). For a more traditional definition, but requiring a dummy variable, see dfss2 3326. Other possible definitions are given by dfss3 3327, dfss4 3563, sspss 3435, ssequn1 3506, ssequn2 3509, sseqin2 3548, and ssdif0 3712. (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 3309 . 2
41, 2cin 3308 . . 3
54, 1wceq 1654 . 2
63, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  dfss  3324  dfss1  3534  inabs  3560  nssinpss  3561  dfrab3ss  3607  disjssun  3711  riinn0  4196  rintn0  4212  ssex  4386  ordtri3or  4654  op1stb  4799  ssdmres  5212  resima2  5223  xpssres  5224  fnimaeq0  5613  fnreseql  5888  curry1  6488  curry2  6491  tpostpos2  6550  sorpssin  6580  tz7.44-2  6714  tz7.44-3  6715  frfnom  6741  ecinxp  7028  infssuni  7446  elfiun  7484  marypha1lem  7487  unxpwdom  7606  cdainf  8123  ackbij1lem16  8166  fin23lem26  8256  isf34lem7  8310  isf34lem6  8311  fpwwe2lem11  8566  fpwwe2lem13  8568  fpwwe2  8569  uzin  10569  iooval2  11000  limsupgle  12322  limsupgre  12326  bitsinv1  13005  bitsres  13036  bitsuz  13037  2prm  13146  dfphi2  13214  ressbas2  13571  ressinbas  13576  ressress  13577  restid2  13709  resscatc  14311  dprdz  15639  dprdcntz2  15647  lmhmlsp  16176  lspdisj2  16250  ressmplbas2  16569  difopn  17149  mretopd  17207  restcld  17287  restopnb  17290  restfpw  17294  neitr  17295  cnrest2  17401  paste  17409  isnrm2  17473  1stccnp  17576  restnlly  17596  lly1stc  17610  kgeni  17620  kgencn3  17641  ptbasfi  17664  hausdiag  17728  qtopval2  17779  qtoprest  17800  filcon  17966  trfil2  17970  trfg  17974  uzrest  17980  trufil  17993  ufileu  18002  fclscf  18108  flimfnfcls  18111  tsmsres  18224  trust  18310  restutopopn  18319  metustfbasOLD  18646  metustfbas  18647  restmetu  18668  xrtgioo  18888  xrsmopn  18894  clsocv  19255  cmetss  19318  ovoliunlem1  19449  difmbl  19488  voliunlem1  19495  volsup2  19548  i1fima  19619  i1fima2  19620  i1fd  19622  itg1addlem5  19641  itg1climres  19655  dvmptid  19894  dvmptc  19895  dvlipcn  19929  dvlip2  19930  dvcnvrelem1  19952  dvcvx  19955  taylthlem1  20340  taylthlem2  20341  psercn  20393  pige3  20476  dvlog  20593  dvcxp1  20677  ppiprm  20985  chtprm  20987  eupares  21748  chm1i  23009  dmdsl3  23869  atssma  23932  dmdbr6ati  23977  imadifxp  24086  sspreima  24105  df1stres  24139  df2ndres  24140  xrge0base  24256  xrge00  24257  esumnul  24492  esumsn  24505  eulerpartlemgs2  24766  probmeasb  24792  ballotlemfp1  24853  cvmscld  25064  cvmliftmolem1  25072  dfon2lem4  25517  dfrdg2  25527  sspred  25551  nodense  25748  fvline2  26184  mblfinlem3  26354  mblfinlem4  26355  ftc1anclem6  26396  dvreasin  26401  areacirclem1  26403  topbnd  26438  opnbnd  26439  neibastop1  26499  subspopn  26569  ssbnd  26608  heiborlem3  26633  elrfi  26929  setindtr  27274  fnwe2lem2  27305  lmhmlnmsplit  27341  pmtrmvd  27554  proot1hash  27675  fgraphopab  27685  dmressnsn  28140  fnresfnco  28145  resisresindm  28253  f0rn0  28257  bnj1322  29435  lcvexchlem3  30074  dihglblem5aN  32330
  Copyright terms: Public domain W3C validator