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

Definition df-ss 3168
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 20816). Note that  A  C_  A (proved in ssid 3199). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3170). For a more traditional definition, but requiring a dummy variable, see dfss2 3171. Other possible definitions are given by dfss3 3172, dfss4 3405, sspss 3277, ssequn1 3347, ssequn2 3350, sseqin2 3390, and ssdif0 3515. (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 3154 . 2  wff  A  C_  B
41, 2cin 3153 . . 3  class  ( A  i^i  B )
54, 1wceq 1625 . 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  3169  dfss1  3375  inabs  3402  nssinpss  3403  dfrab3ss  3448  disjssun  3514  riinn0  3978  rintn0  3994  ssex  4160  ordtri3or  4426  op1stb  4571  ssdmres  4979  resima2  4990  xpssres  4991  fnimaeq0  5367  fnreseql  5637  curry1  6212  curry2  6215  tpostpos2  6257  sorpssin  6287  tz7.44-2  6422  tz7.44-3  6423  frfnom  6449  ecinxp  6736  elfiun  7185  marypha1lem  7188  unxpwdom  7305  cdainf  7820  ackbij1lem16  7863  fin23lem26  7953  isf34lem7  8007  isf34lem6  8008  fpwwe2lem11  8264  fpwwe2lem13  8266  fpwwe2  8267  uzin  10262  iooval2  10691  limsupgle  11953  limsupgre  11957  incexclem  12297  incexc  12298  bitsinv1  12635  bitsres  12666  bitsuz  12667  2prm  12776  dfphi2  12844  ressbas2  13201  ressinbas  13206  ressress  13207  restid2  13337  resscatc  13939  dprdz  15267  dprdcntz2  15275  lmhmlsp  15808  lspdisj2  15882  ressmplbas2  16201  difopn  16773  mretopd  16831  restcld  16905  restopnb  16908  restfpw  16912  cnrest2  17016  paste  17024  isnrm2  17088  1stccnp  17190  restnlly  17210  lly1stc  17224  kgeni  17234  kgencn3  17255  ptbasfi  17278  hausdiag  17341  qtopval2  17389  qtoprest  17410  filcon  17580  trfil2  17584  trfg  17588  uzrest  17594  trufil  17607  ufileu  17616  fclscf  17722  flimfnfcls  17725  tsmsres  17828  xrtgioo  18314  xrsmopn  18320  clsocv  18679  cmetss  18742  ovoliunlem1  18863  difmbl  18902  voliunlem1  18909  volsup2  18962  i1fima  19035  i1fima2  19036  i1fd  19038  itg1addlem5  19057  itg1climres  19071  dvmptid  19308  dvmptc  19309  dvlipcn  19343  dvlip2  19344  dvcnvrelem1  19366  dvcvx  19369  taylthlem1  19754  taylthlem2  19755  psercn  19804  pige3  19887  dvlog  20000  dvcxp1  20084  ppiprm  20391  chtprm  20393  chm1i  22037  dmdsl3  22897  atssma  22960  dmdbr6ati  23005  ballotlemfp1  23052  ballotlemfmpn  23055  sspreima  23212  df1stres  23245  df2ndres  23246  xrge0base  23312  xrge00  23313  esumnul  23429  esumsn  23439  totprobd  23631  probmeasb  23635  cvmscld  23806  cvmliftmolem1  23814  eupares  23901  dfon2lem4  24144  dfrdg2  24154  sspred  24176  nodense  24345  fvline2  24771  dvreasin  24925  areacirclem2  24936  areacirclem3  24937  isunscov  25085  domrancur1b  25211  domrancur1c  25213  basexre  25533  islimrs4  25593  topbnd  26253  opnbnd  26254  neibastop1  26319  subspopn  26477  ssbnd  26523  heiborlem3  26548  elrfi  26780  setindtr  27128  fnwe2lem2  27159  lmhmlnmsplit  27196  pmtrmvd  27409  proot1hash  27530  fgraphopab  27540  dmressnsn  27994  fnresfnco  28000  funcoressn  28001  funressnfv  28002  bnj1322  28928  lcvexchlem3  29299  dihglblem5aN  31555
  Copyright terms: Public domain W3C validator