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

Definition df-ss 3326
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 21727). Note that  A  C_  A (proved in ssid 3359). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3328). For a more traditional definition, but requiring a dummy variable, see dfss2 3329. Other possible definitions are given by dfss3 3330, dfss4 3567, sspss 3438, ssequn1 3509, ssequn2 3512, sseqin2 3552, and ssdif0 3678. (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 3312 . 2  wff  A  C_  B
41, 2cin 3311 . . 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  3327  dfss1  3537  inabs  3564  nssinpss  3565  dfrab3ss  3611  disjssun  3677  riinn0  4157  rintn0  4173  ssex  4339  ordtri3or  4605  op1stb  4750  ssdmres  5160  resima2  5171  xpssres  5172  fnimaeq0  5558  fnreseql  5832  curry1  6430  curry2  6433  tpostpos2  6492  sorpssin  6522  tz7.44-2  6657  tz7.44-3  6658  frfnom  6684  ecinxp  6971  infssuni  7389  elfiun  7427  marypha1lem  7430  unxpwdom  7549  cdainf  8064  ackbij1lem16  8107  fin23lem26  8197  isf34lem7  8251  isf34lem6  8252  fpwwe2lem11  8507  fpwwe2lem13  8509  fpwwe2  8510  uzin  10510  iooval2  10941  limsupgle  12263  limsupgre  12267  bitsinv1  12946  bitsres  12977  bitsuz  12978  2prm  13087  dfphi2  13155  ressbas2  13512  ressinbas  13517  ressress  13518  restid2  13650  resscatc  14252  dprdz  15580  dprdcntz2  15588  lmhmlsp  16117  lspdisj2  16191  ressmplbas2  16510  difopn  17090  mretopd  17148  restcld  17228  restopnb  17231  restfpw  17235  neitr  17236  cnrest2  17342  paste  17350  isnrm2  17414  1stccnp  17517  restnlly  17537  lly1stc  17551  kgeni  17561  kgencn3  17582  ptbasfi  17605  hausdiag  17669  qtopval2  17720  qtoprest  17741  filcon  17907  trfil2  17911  trfg  17915  uzrest  17921  trufil  17934  ufileu  17943  fclscf  18049  flimfnfcls  18052  tsmsres  18165  trust  18251  restutopopn  18260  metustfbasOLD  18587  metustfbas  18588  restmetu  18609  xrtgioo  18829  xrsmopn  18835  clsocv  19196  cmetss  19259  ovoliunlem1  19390  difmbl  19429  voliunlem1  19436  volsup2  19489  i1fima  19562  i1fima2  19563  i1fd  19565  itg1addlem5  19584  itg1climres  19598  dvmptid  19835  dvmptc  19836  dvlipcn  19870  dvlip2  19871  dvcnvrelem1  19893  dvcvx  19896  taylthlem1  20281  taylthlem2  20282  psercn  20334  pige3  20417  dvlog  20534  dvcxp1  20618  ppiprm  20926  chtprm  20928  eupares  21689  chm1i  22950  dmdsl3  23810  atssma  23873  dmdbr6ati  23918  imadifxp  24030  sspreima  24049  df1stres  24083  df2ndres  24084  xrge0base  24199  xrge00  24200  esumnul  24435  esumsn  24448  probmeasb  24680  ballotlemfp1  24741  cvmscld  24952  cvmliftmolem1  24960  dfon2lem4  25405  dfrdg2  25415  sspred  25439  nodense  25636  fvline2  26072  mblfinlem2  26235  mblfinlem3  26236  ftc1anclem6  26275  dvreasin  26280  areacirclem2  26282  areacirclem3  26283  topbnd  26318  opnbnd  26319  neibastop1  26379  subspopn  26449  ssbnd  26488  heiborlem3  26513  elrfi  26739  setindtr  27086  fnwe2lem2  27117  lmhmlnmsplit  27153  pmtrmvd  27366  proot1hash  27487  fgraphopab  27497  dmressnsn  27952  fnresfnco  27957  resisresindm  28061  bnj1322  29131  lcvexchlem3  29771  dihglblem5aN  32027
  Copyright terms: Public domain W3C validator