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

Definition df-ss 3278
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 21584). Note that  A  C_  A (proved in ssid 3311). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3280). For a more traditional definition, but requiring a dummy variable, see dfss2 3281. Other possible definitions are given by dfss3 3282, dfss4 3519, sspss 3390, ssequn1 3461, ssequn2 3464, sseqin2 3504, and ssdif0 3630. (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 3264 . 2  wff  A  C_  B
41, 2cin 3263 . . 3  class  ( A  i^i  B )
54, 1wceq 1649 . 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  3279  dfss1  3489  inabs  3516  nssinpss  3517  dfrab3ss  3563  disjssun  3629  riinn0  4107  rintn0  4123  ssex  4289  ordtri3or  4555  op1stb  4699  ssdmres  5109  resima2  5120  xpssres  5121  fnimaeq0  5507  fnreseql  5780  curry1  6378  curry2  6381  tpostpos2  6437  sorpssin  6467  tz7.44-2  6602  tz7.44-3  6603  frfnom  6629  ecinxp  6916  elfiun  7371  marypha1lem  7374  unxpwdom  7491  cdainf  8006  ackbij1lem16  8049  fin23lem26  8139  isf34lem7  8193  isf34lem6  8194  fpwwe2lem11  8449  fpwwe2lem13  8451  fpwwe2  8452  uzin  10451  iooval2  10882  limsupgle  12199  limsupgre  12203  bitsinv1  12882  bitsres  12913  bitsuz  12914  2prm  13023  dfphi2  13091  ressbas2  13448  ressinbas  13453  ressress  13454  restid2  13586  resscatc  14188  dprdz  15516  dprdcntz2  15524  lmhmlsp  16053  lspdisj2  16127  ressmplbas2  16446  difopn  17022  mretopd  17080  restcld  17159  restopnb  17162  restfpw  17166  neitr  17167  cnrest2  17273  paste  17281  isnrm2  17345  1stccnp  17447  restnlly  17467  lly1stc  17481  kgeni  17491  kgencn3  17512  ptbasfi  17535  hausdiag  17599  qtopval2  17650  qtoprest  17671  filcon  17837  trfil2  17841  trfg  17845  uzrest  17851  trufil  17864  ufileu  17873  fclscf  17979  flimfnfcls  17982  tsmsres  18095  trust  18181  restutopopn  18190  metustfbas  18478  restmetu  18490  xrtgioo  18709  xrsmopn  18715  clsocv  19076  cmetss  19139  ovoliunlem1  19266  difmbl  19305  voliunlem1  19312  volsup2  19365  i1fima  19438  i1fima2  19439  i1fd  19441  itg1addlem5  19460  itg1climres  19474  dvmptid  19711  dvmptc  19712  dvlipcn  19746  dvlip2  19747  dvcnvrelem1  19769  dvcvx  19772  taylthlem1  20157  taylthlem2  20158  psercn  20210  pige3  20293  dvlog  20410  dvcxp1  20494  ppiprm  20802  chtprm  20804  eupares  21546  chm1i  22807  dmdsl3  23667  atssma  23730  dmdbr6ati  23775  imadifxp  23882  sspreima  23900  df1stres  23933  df2ndres  23934  xrge0base  24037  xrge00  24038  esumnul  24240  esumsn  24253  probmeasb  24468  ballotlemfp1  24529  cvmscld  24740  cvmliftmolem1  24748  dfon2lem4  25167  dfrdg2  25177  sspred  25199  nodense  25368  fvline2  25795  dvreasin  25981  areacirclem2  25983  areacirclem3  25984  topbnd  26019  opnbnd  26020  neibastop1  26080  subspopn  26150  ssbnd  26189  heiborlem3  26214  elrfi  26440  setindtr  26787  fnwe2lem2  26818  lmhmlnmsplit  26855  pmtrmvd  27068  proot1hash  27189  fgraphopab  27199  dmressnsn  27654  fnresfnco  27660  bnj1322  28533  lcvexchlem3  29152  dihglblem5aN  31408
  Copyright terms: Public domain W3C validator