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

Definition df-ss 3108
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 20722). Note that  A  C_  A (proved in ssid 3139). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3110). For a more traditional definition, but requiring a dummy variable, see dfss2 3111. Other possible definitions are given by dfss3 3112, dfss4 3345, sspss 3217, ssequn1 3287, ssequn2 3290, sseqin2 3330, and ssdif0 3455. (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 3094 . 2  wff  A  C_  B
41, 2cin 3093 . . 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  3109  dfss1  3315  inabs  3342  nssinpss  3343  dfrab3ss  3388  disjssun  3454  riinn0  3917  rintn0  3933  ssex  4098  ordtri3or  4361  op1stb  4506  ssdmres  4930  resima2  4941  xpssres  4942  fnimaeq0  5268  fnreseql  5534  curry1  6109  curry2  6112  tpostpos2  6154  sorpssin  6184  tz7.44-2  6353  tz7.44-3  6354  frfnom  6380  ecinxp  6667  elfiun  7116  marypha1lem  7119  unxpwdom  7236  cdainf  7751  ackbij1lem16  7794  fin23lem26  7884  isf34lem7  7938  isf34lem6  7939  fpwwe2lem11  8195  fpwwe2lem13  8197  fpwwe2  8198  uzin  10192  iooval2  10620  limsupgle  11881  limsupgre  11885  bitsinv1  12560  bitsres  12591  bitsuz  12592  2prm  12701  dfphi2  12769  ressbas2  13126  ressinbas  13131  ressress  13132  restid2  13262  resscatc  13864  dprdz  15192  dprdcntz2  15200  lmhmlsp  15733  lspdisj2  15807  ressmplbas2  16126  difopn  16698  mretopd  16756  restcld  16830  restopnb  16833  restfpw  16837  cnrest2  16941  paste  16949  isnrm2  17013  1stccnp  17115  restnlly  17135  lly1stc  17149  kgeni  17159  kgencn3  17180  ptbasfi  17203  hausdiag  17266  qtopval2  17314  qtoprest  17335  filcon  17505  trfil2  17509  trfg  17513  uzrest  17519  trufil  17532  ufileu  17541  fclscf  17647  flimfnfcls  17650  tsmsres  17753  xrtgioo  18239  xrsmopn  18245  clsocv  18604  cmetss  18667  ovoliunlem1  18788  difmbl  18827  voliunlem1  18834  volsup2  18887  i1fima  18960  i1fima2  18961  i1fd  18963  itg1addlem5  18982  itg1climres  18996  dvmptid  19233  dvmptc  19234  dvlipcn  19268  dvlip2  19269  dvcnvrelem1  19291  dvcvx  19294  taylthlem1  19679  taylthlem2  19680  psercn  19729  pige3  19812  dvlog  19925  dvcxp1  20009  ppiprm  20316  chtprm  20318  chm1i  21960  dmdsl3  22820  atssma  22883  dmdbr6ati  22928  ballotlemfp1  22976  ballotlemfmpn  22979  cvmscld  23141  cvmliftmolem1  23149  eupares  23236  dfon2lem4  23476  dfrdg2  23486  sspred  23508  axdense  23677  fvline2  24109  isunscov  24405  domrancur1b  24532  domrancur1c  24534  basexre  24854  islimrs4  24914  topbnd  25574  opnbnd  25575  neibastop1  25640  subspopn  25798  ssbnd  25844  heiborlem3  25869  elrfi  26101  setindtr  26449  fnwe2lem2  26480  lmhmlnmsplit  26517  pmtrmvd  26730  proot1hash  26851  fgraphopab  26861  bnj1322  27867  lcvexchlem3  28356  dihglblem5aN  30612
  Copyright terms: Public domain W3C validator