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

Definition df-ss 3336
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 21740). Note that  A  C_  A (proved in ssid 3369). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3338). For a more traditional definition, but requiring a dummy variable, see dfss2 3339. Other possible definitions are given by dfss3 3340, dfss4 3577, sspss 3448, ssequn1 3519, ssequn2 3522, sseqin2 3562, and ssdif0 3688. (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 3322 . 2  wff  A  C_  B
41, 2cin 3321 . . 3  class  ( A  i^i  B )
54, 1wceq 1653 . 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  3337  dfss1  3547  inabs  3574  nssinpss  3575  dfrab3ss  3621  disjssun  3687  riinn0  4168  rintn0  4184  ssex  4350  ordtri3or  4616  op1stb  4761  ssdmres  5171  resima2  5182  xpssres  5183  fnimaeq0  5569  fnreseql  5843  curry1  6441  curry2  6444  tpostpos2  6503  sorpssin  6533  tz7.44-2  6668  tz7.44-3  6669  frfnom  6695  ecinxp  6982  infssuni  7400  elfiun  7438  marypha1lem  7441  unxpwdom  7560  cdainf  8077  ackbij1lem16  8120  fin23lem26  8210  isf34lem7  8264  isf34lem6  8265  fpwwe2lem11  8520  fpwwe2lem13  8522  fpwwe2  8523  uzin  10523  iooval2  10954  limsupgle  12276  limsupgre  12280  bitsinv1  12959  bitsres  12990  bitsuz  12991  2prm  13100  dfphi2  13168  ressbas2  13525  ressinbas  13530  ressress  13531  restid2  13663  resscatc  14265  dprdz  15593  dprdcntz2  15601  lmhmlsp  16130  lspdisj2  16204  ressmplbas2  16523  difopn  17103  mretopd  17161  restcld  17241  restopnb  17244  restfpw  17248  neitr  17249  cnrest2  17355  paste  17363  isnrm2  17427  1stccnp  17530  restnlly  17550  lly1stc  17564  kgeni  17574  kgencn3  17595  ptbasfi  17618  hausdiag  17682  qtopval2  17733  qtoprest  17754  filcon  17920  trfil2  17924  trfg  17928  uzrest  17934  trufil  17947  ufileu  17956  fclscf  18062  flimfnfcls  18065  tsmsres  18178  trust  18264  restutopopn  18273  metustfbasOLD  18600  metustfbas  18601  restmetu  18622  xrtgioo  18842  xrsmopn  18848  clsocv  19209  cmetss  19272  ovoliunlem1  19403  difmbl  19442  voliunlem1  19449  volsup2  19502  i1fima  19573  i1fima2  19574  i1fd  19576  itg1addlem5  19595  itg1climres  19609  dvmptid  19848  dvmptc  19849  dvlipcn  19883  dvlip2  19884  dvcnvrelem1  19906  dvcvx  19909  taylthlem1  20294  taylthlem2  20295  psercn  20347  pige3  20430  dvlog  20547  dvcxp1  20631  ppiprm  20939  chtprm  20941  eupares  21702  chm1i  22963  dmdsl3  23823  atssma  23886  dmdbr6ati  23931  imadifxp  24043  sspreima  24062  df1stres  24096  df2ndres  24097  xrge0base  24212  xrge00  24213  esumnul  24448  esumsn  24461  probmeasb  24693  ballotlemfp1  24754  cvmscld  24965  cvmliftmolem1  24973  dfon2lem4  25418  dfrdg2  25428  sspred  25452  nodense  25649  fvline2  26085  mblfinlem3  26257  mblfinlem4  26258  ftc1anclem6  26299  dvreasin  26304  areacirclem1  26306  topbnd  26341  opnbnd  26342  neibastop1  26402  subspopn  26472  ssbnd  26511  heiborlem3  26536  elrfi  26762  setindtr  27109  fnwe2lem2  27140  lmhmlnmsplit  27176  pmtrmvd  27389  proot1hash  27510  fgraphopab  27520  dmressnsn  27975  fnresfnco  27980  resisresindm  28089  f0rn0  28093  bnj1322  29268  lcvexchlem3  29908  dihglblem5aN  32164
  Copyright terms: Public domain W3C validator