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

Definition df-ss 3179
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 20830). Note that  A  C_  A (proved in ssid 3210). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3181). For a more traditional definition, but requiring a dummy variable, see dfss2 3182. Other possible definitions are given by dfss3 3183, dfss4 3416, sspss 3288, ssequn1 3358, ssequn2 3361, sseqin2 3401, and ssdif0 3526. (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 3165 . 2  wff  A  C_  B
41, 2cin 3164 . . 3  class  ( A  i^i  B )
54, 1wceq 1632 . 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  3180  dfss1  3386  inabs  3413  nssinpss  3414  dfrab3ss  3459  disjssun  3525  riinn0  3992  rintn0  4008  ssex  4174  ordtri3or  4440  op1stb  4585  ssdmres  4993  resima2  5004  xpssres  5005  fnimaeq0  5381  fnreseql  5651  curry1  6226  curry2  6229  tpostpos2  6271  sorpssin  6301  tz7.44-2  6436  tz7.44-3  6437  frfnom  6463  ecinxp  6750  elfiun  7199  marypha1lem  7202  unxpwdom  7319  cdainf  7834  ackbij1lem16  7877  fin23lem26  7967  isf34lem7  8021  isf34lem6  8022  fpwwe2lem11  8278  fpwwe2lem13  8280  fpwwe2  8281  uzin  10276  iooval2  10705  limsupgle  11967  limsupgre  11971  incexclem  12311  incexc  12312  bitsinv1  12649  bitsres  12680  bitsuz  12681  2prm  12790  dfphi2  12858  ressbas2  13215  ressinbas  13220  ressress  13221  restid2  13351  resscatc  13953  dprdz  15281  dprdcntz2  15289  lmhmlsp  15822  lspdisj2  15896  ressmplbas2  16215  difopn  16787  mretopd  16845  restcld  16919  restopnb  16922  restfpw  16926  cnrest2  17030  paste  17038  isnrm2  17102  1stccnp  17204  restnlly  17224  lly1stc  17238  kgeni  17248  kgencn3  17269  ptbasfi  17292  hausdiag  17355  qtopval2  17403  qtoprest  17424  filcon  17594  trfil2  17598  trfg  17602  uzrest  17608  trufil  17621  ufileu  17630  fclscf  17736  flimfnfcls  17739  tsmsres  17842  xrtgioo  18328  xrsmopn  18334  clsocv  18693  cmetss  18756  ovoliunlem1  18877  difmbl  18916  voliunlem1  18923  volsup2  18976  i1fima  19049  i1fima2  19050  i1fd  19052  itg1addlem5  19071  itg1climres  19085  dvmptid  19322  dvmptc  19323  dvlipcn  19357  dvlip2  19358  dvcnvrelem1  19380  dvcvx  19383  taylthlem1  19768  taylthlem2  19769  psercn  19818  pige3  19901  dvlog  20014  dvcxp1  20098  ppiprm  20405  chtprm  20407  chm1i  22051  dmdsl3  22911  atssma  22974  dmdbr6ati  23019  ballotlemfp1  23066  ballotlemfmpn  23069  sspreima  23225  df1stres  23258  df2ndres  23259  xrge0base  23325  xrge00  23326  esumnul  23442  esumsn  23452  totprobd  23644  probmeasb  23648  cvmscld  23819  cvmliftmolem1  23827  eupares  23914  dfon2lem4  24213  dfrdg2  24223  sspred  24245  nodense  24414  fvline2  24841  dvreasin  25026  areacirclem2  25028  areacirclem3  25029  isunscov  25177  domrancur1b  25303  domrancur1c  25305  basexre  25625  islimrs4  25685  topbnd  26345  opnbnd  26346  neibastop1  26411  subspopn  26569  ssbnd  26615  heiborlem3  26640  elrfi  26872  setindtr  27220  fnwe2lem2  27251  lmhmlnmsplit  27288  pmtrmvd  27501  proot1hash  27622  fgraphopab  27632  dmressnsn  28088  fnresfnco  28094  funcoressn  28095  funressnfv  28096  bnj1322  29171  lcvexchlem3  29848  dihglblem5aN  32104
  Copyright terms: Public domain W3C validator