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

Definition df-ss 3334
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 21735). Note that  A  C_  A (proved in ssid 3367). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3336). For a more traditional definition, but requiring a dummy variable, see dfss2 3337. Other possible definitions are given by dfss3 3338, dfss4 3575, sspss 3446, ssequn1 3517, ssequn2 3520, sseqin2 3560, and ssdif0 3686. (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
df-ss  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wss 3320 . 2  wff  A  C_  B
41, 2cin 3319 . . 3  class  ( A  i^i  B )
54, 1wceq 1652 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 177 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  3335  dfss1  3545  inabs  3572  nssinpss  3573  dfrab3ss  3619  disjssun  3685  riinn0  4165  rintn0  4181  ssex  4347  ordtri3or  4613  op1stb  4758  ssdmres  5168  resima2  5179  xpssres  5180  fnimaeq0  5566  fnreseql  5840  curry1  6438  curry2  6441  tpostpos2  6500  sorpssin  6530  tz7.44-2  6665  tz7.44-3  6666  frfnom  6692  ecinxp  6979  infssuni  7397  elfiun  7435  marypha1lem  7438  unxpwdom  7557  cdainf  8072  ackbij1lem16  8115  fin23lem26  8205  isf34lem7  8259  isf34lem6  8260  fpwwe2lem11  8515  fpwwe2lem13  8517  fpwwe2  8518  uzin  10518  iooval2  10949  limsupgle  12271  limsupgre  12275  bitsinv1  12954  bitsres  12985  bitsuz  12986  2prm  13095  dfphi2  13163  ressbas2  13520  ressinbas  13525  ressress  13526  restid2  13658  resscatc  14260  dprdz  15588  dprdcntz2  15596  lmhmlsp  16125  lspdisj2  16199  ressmplbas2  16518  difopn  17098  mretopd  17156  restcld  17236  restopnb  17239  restfpw  17243  neitr  17244  cnrest2  17350  paste  17358  isnrm2  17422  1stccnp  17525  restnlly  17545  lly1stc  17559  kgeni  17569  kgencn3  17590  ptbasfi  17613  hausdiag  17677  qtopval2  17728  qtoprest  17749  filcon  17915  trfil2  17919  trfg  17923  uzrest  17929  trufil  17942  ufileu  17951  fclscf  18057  flimfnfcls  18060  tsmsres  18173  trust  18259  restutopopn  18268  metustfbasOLD  18595  metustfbas  18596  restmetu  18617  xrtgioo  18837  xrsmopn  18843  clsocv  19204  cmetss  19267  ovoliunlem1  19398  difmbl  19437  voliunlem1  19444  volsup2  19497  i1fima  19570  i1fima2  19571  i1fd  19573  itg1addlem5  19592  itg1climres  19606  dvmptid  19843  dvmptc  19844  dvlipcn  19878  dvlip2  19879  dvcnvrelem1  19901  dvcvx  19904  taylthlem1  20289  taylthlem2  20290  psercn  20342  pige3  20425  dvlog  20542  dvcxp1  20626  ppiprm  20934  chtprm  20936  eupares  21697  chm1i  22958  dmdsl3  23818  atssma  23881  dmdbr6ati  23926  imadifxp  24038  sspreima  24057  df1stres  24091  df2ndres  24092  xrge0base  24207  xrge00  24208  esumnul  24443  esumsn  24456  probmeasb  24688  ballotlemfp1  24749  cvmscld  24960  cvmliftmolem1  24968  dfon2lem4  25413  dfrdg2  25423  sspred  25447  nodense  25644  fvline2  26080  mblfinlem3  26245  mblfinlem4  26246  ftc1anclem6  26285  dvreasin  26290  areacirclem1  26292  topbnd  26327  opnbnd  26328  neibastop1  26388  subspopn  26458  ssbnd  26497  heiborlem3  26522  elrfi  26748  setindtr  27095  fnwe2lem2  27126  lmhmlnmsplit  27162  pmtrmvd  27375  proot1hash  27496  fgraphopab  27506  dmressnsn  27961  fnresfnco  27966  resisresindm  28074  bnj1322  29194  lcvexchlem3  29834  dihglblem5aN  32090
  Copyright terms: Public domain W3C validator