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

Definition df-ss 3141
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 20758). Note that  A  C_  A (proved in ssid 3172). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3143). For a more traditional definition, but requiring a dummy variable, see dfss2 3144. Other possible definitions are given by dfss3 3145, dfss4 3378, sspss 3250, ssequn1 3320, ssequn2 3323, sseqin2 3363, and ssdif0 3488. (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 3127 . 2  wff  A  C_  B
41, 2cin 3126 . . 3  class  ( A  i^i  B )
54, 1wceq 1619 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 178 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  3142  dfss1  3348  inabs  3375  nssinpss  3376  dfrab3ss  3421  disjssun  3487  riinn0  3950  rintn0  3966  ssex  4132  ordtri3or  4396  op1stb  4541  ssdmres  4965  resima2  4976  xpssres  4977  fnimaeq0  5303  fnreseql  5569  curry1  6144  curry2  6147  tpostpos2  6189  sorpssin  6219  tz7.44-2  6388  tz7.44-3  6389  frfnom  6415  ecinxp  6702  elfiun  7151  marypha1lem  7154  unxpwdom  7271  cdainf  7786  ackbij1lem16  7829  fin23lem26  7919  isf34lem7  7973  isf34lem6  7974  fpwwe2lem11  8230  fpwwe2lem13  8232  fpwwe2  8233  uzin  10228  iooval2  10656  limsupgle  11917  limsupgre  11921  bitsinv1  12596  bitsres  12627  bitsuz  12628  2prm  12737  dfphi2  12805  ressbas2  13162  ressinbas  13167  ressress  13168  restid2  13298  resscatc  13900  dprdz  15228  dprdcntz2  15236  lmhmlsp  15769  lspdisj2  15843  ressmplbas2  16162  difopn  16734  mretopd  16792  restcld  16866  restopnb  16869  restfpw  16873  cnrest2  16977  paste  16985  isnrm2  17049  1stccnp  17151  restnlly  17171  lly1stc  17185  kgeni  17195  kgencn3  17216  ptbasfi  17239  hausdiag  17302  qtopval2  17350  qtoprest  17371  filcon  17541  trfil2  17545  trfg  17549  uzrest  17555  trufil  17568  ufileu  17577  fclscf  17683  flimfnfcls  17686  tsmsres  17789  xrtgioo  18275  xrsmopn  18281  clsocv  18640  cmetss  18703  ovoliunlem1  18824  difmbl  18863  voliunlem1  18870  volsup2  18923  i1fima  18996  i1fima2  18997  i1fd  18999  itg1addlem5  19018  itg1climres  19032  dvmptid  19269  dvmptc  19270  dvlipcn  19304  dvlip2  19305  dvcnvrelem1  19327  dvcvx  19330  taylthlem1  19715  taylthlem2  19716  psercn  19765  pige3  19848  dvlog  19961  dvcxp1  20045  ppiprm  20352  chtprm  20354  chm1i  21996  dmdsl3  22856  atssma  22919  dmdbr6ati  22964  ballotlemfp1  23012  ballotlemfmpn  23015  cvmscld  23177  cvmliftmolem1  23185  eupares  23272  dfon2lem4  23512  dfrdg2  23522  sspred  23544  axdense  23713  fvline2  24145  isunscov  24441  domrancur1b  24568  domrancur1c  24570  basexre  24890  islimrs4  24950  topbnd  25610  opnbnd  25611  neibastop1  25676  subspopn  25834  ssbnd  25880  heiborlem3  25905  elrfi  26137  setindtr  26485  fnwe2lem2  26516  lmhmlnmsplit  26553  pmtrmvd  26766  proot1hash  26887  fgraphopab  26897  bnj1322  27987  lcvexchlem3  28476  dihglblem5aN  30732
  Copyright terms: Public domain W3C validator