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

Definition df-ss 3089
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 20627). Note that  A  C_  A (proved in ssid 3118). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3091). For a more traditional definition, but requiring a dummy variable, see dfss2 3092. Other possible definitions are given by dfss3 3093, dfss4 3310, sspss 3195, ssequn1 3255, ssequn2 3258, sseqin2 3295, and ssdif0 3420. (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 3078 . 2  wff  A  C_  B
41, 2cin 3077 . . 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  3090  dfss1  3281  inabs  3307  nssinpss  3308  dfrab3ss  3353  disjssun  3419  riinn0  3874  rintn0  3890  ssex  4055  ordtri3or  4317  op1stb  4460  ssdmres  4884  resima2  4895  xpssres  4896  fnimaeq0  5222  fnreseql  5487  curry1  6062  curry2  6065  tpostpos2  6107  sorpssin  6137  tz7.44-2  6306  tz7.44-3  6307  frfnom  6333  ecinxp  6620  elfiun  7067  marypha1lem  7070  unxpwdom  7187  cdainf  7702  ackbij1lem16  7745  fin23lem26  7835  isf34lem7  7889  isf34lem6  7890  fpwwe2lem11  8142  fpwwe2lem13  8144  fpwwe2  8145  uzin  10139  iooval2  10567  limsupgle  11828  limsupgre  11832  bitsinv1  12507  bitsres  12538  bitsuz  12539  2prm  12648  dfphi2  12716  ressbas2  13073  ressinbas  13078  ressress  13079  restid2  13209  resscatc  13781  dprdz  15100  dprdcntz2  15108  lmhmlsp  15641  lspdisj2  15715  ressmplbas2  16031  difopn  16603  mretopd  16661  restcld  16735  restopnb  16738  restfpw  16742  cnrest2  16846  paste  16854  isnrm2  16918  1stccnp  17020  restnlly  17040  lly1stc  17054  kgeni  17064  kgencn3  17085  ptbasfi  17108  hausdiag  17171  qtopval2  17219  qtoprest  17240  filcon  17410  trfil2  17414  trfg  17418  uzrest  17424  trufil  17437  ufileu  17446  fclscf  17552  flimfnfcls  17555  tsmsres  17658  xrtgioo  18144  xrsmopn  18150  clsocv  18509  cmetss  18572  ovoliunlem1  18693  difmbl  18732  voliunlem1  18739  volsup2  18792  i1fima  18865  i1fima2  18866  i1fd  18868  itg1addlem5  18887  itg1climres  18901  dvmptid  19138  dvmptc  19139  dvlipcn  19173  dvlip2  19174  dvcnvrelem1  19196  dvcvx  19199  taylthlem1  19584  taylthlem2  19585  psercn  19634  pige3  19717  dvlog  19830  dvcxp1  19950  ppiprm  20221  chtprm  20223  chm1i  21865  dmdsl3  22725  atssma  22788  dmdbr6ati  22833  cvmscld  22975  cvmliftmolem1  22983  eupares  23070  dfon2lem4  23310  dfrdg2  23320  sspred  23342  axdense  23511  fvline2  23943  isunscov  24239  domrancur1b  24366  domrancur1c  24368  basexre  24688  islimrs4  24748  topbnd  25408  opnbnd  25409  neibastop1  25474  subspopn  25632  ssbnd  25678  heiborlem3  25703  elrfi  25935  setindtr  26283  fnwe2lem2  26314  lmhmlnmsplit  26351  pmtrmvd  26564  proot1hash  26685  fgraphopab  26695  bnj1322  27544  lcvexchlem3  27915  dihglblem5aN  30171
  Copyright terms: Public domain W3C validator