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

Definition df-ss 3167
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 20791). Note that  A  C_  A (proved in ssid 3198). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3169). For a more traditional definition, but requiring a dummy variable, see dfss2 3170. Other possible definitions are given by dfss3 3171, dfss4 3404, sspss 3276, ssequn1 3346, ssequn2 3349, sseqin2 3389, and ssdif0 3514. (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 3153 . 2  wff  A  C_  B
41, 2cin 3152 . . 3  class  ( A  i^i  B )
54, 1wceq 1623 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 176 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  3168  dfss1  3374  inabs  3401  nssinpss  3402  dfrab3ss  3447  disjssun  3513  riinn0  3977  rintn0  3993  ssex  4159  ordtri3or  4423  op1stb  4568  ssdmres  4976  resima2  4987  xpssres  4988  fnimaeq0  5331  fnreseql  5597  curry1  6172  curry2  6175  tpostpos2  6217  sorpssin  6247  tz7.44-2  6416  tz7.44-3  6417  frfnom  6443  ecinxp  6730  elfiun  7179  marypha1lem  7182  unxpwdom  7299  cdainf  7814  ackbij1lem16  7857  fin23lem26  7947  isf34lem7  8001  isf34lem6  8002  fpwwe2lem11  8258  fpwwe2lem13  8260  fpwwe2  8261  uzin  10256  iooval2  10685  limsupgle  11947  limsupgre  11951  incexclem  12291  incexc  12292  bitsinv1  12629  bitsres  12660  bitsuz  12661  2prm  12770  dfphi2  12838  ressbas2  13195  ressinbas  13200  ressress  13201  restid2  13331  resscatc  13933  dprdz  15261  dprdcntz2  15269  lmhmlsp  15802  lspdisj2  15876  ressmplbas2  16195  difopn  16767  mretopd  16825  restcld  16899  restopnb  16902  restfpw  16906  cnrest2  17010  paste  17018  isnrm2  17082  1stccnp  17184  restnlly  17204  lly1stc  17218  kgeni  17228  kgencn3  17249  ptbasfi  17272  hausdiag  17335  qtopval2  17383  qtoprest  17404  filcon  17574  trfil2  17578  trfg  17582  uzrest  17588  trufil  17601  ufileu  17610  fclscf  17716  flimfnfcls  17719  tsmsres  17822  xrtgioo  18308  xrsmopn  18314  clsocv  18673  cmetss  18736  ovoliunlem1  18857  difmbl  18896  voliunlem1  18903  volsup2  18956  i1fima  19029  i1fima2  19030  i1fd  19032  itg1addlem5  19051  itg1climres  19065  dvmptid  19302  dvmptc  19303  dvlipcn  19337  dvlip2  19338  dvcnvrelem1  19360  dvcvx  19363  taylthlem1  19748  taylthlem2  19749  psercn  19798  pige3  19881  dvlog  19994  dvcxp1  20078  ppiprm  20385  chtprm  20387  chm1i  22031  dmdsl3  22891  atssma  22954  dmdbr6ati  22999  ballotlemfp1  23046  ballotlemfmpn  23049  cvmscld  23211  cvmliftmolem1  23219  eupares  23306  dfon2lem4  23546  dfrdg2  23556  sspred  23578  axdense  23747  fvline2  24179  dvreasin  24333  areacirclem2  24335  areacirclem3  24336  isunscov  24484  domrancur1b  24611  domrancur1c  24613  basexre  24933  islimrs4  24993  topbnd  25653  opnbnd  25654  neibastop1  25719  subspopn  25877  ssbnd  25923  heiborlem3  25948  elrfi  26180  setindtr  26528  fnwe2lem2  26559  lmhmlnmsplit  26596  pmtrmvd  26809  proot1hash  26930  fgraphopab  26940  dmressnsn  27374  fnresfnco  27380  funcoressn  27381  funressnfv  27382  bnj1322  28134  lcvexchlem3  28505  dihglblem5aN  30761
  Copyright terms: Public domain W3C validator