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

Definition df-ss 3379
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, (ex-ss 22756). Note that (proved in ssid 3412). Contrast this relationship with the relationship (as will be defined in df-pss 3381). For a more traditional definition, but requiring a dummy variable, see dfss2 3382. Other possible definitions are given by dfss3 3383, dfss4 3620, sspss 3492, ssequn1 3563, ssequn2 3566, sseqin2 3605, and ssdif0 3772. (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
df-ss

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wss 3365 . 2
41, 2cin 3364 . . 3
54, 1wceq 1670 . 2
63, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  dfss  3380  dfss1  3591  inabs  3617  nssinpss  3618  dfrab3ss  3664  disjssun  3771  riinn0  4271  rintn0  4287  ssex  4462  op1stb  4585  ordtri3or  4772  ssdmres  5155  resima2  5166  xpssres  5167  fnimaeq0  5550  fnreseql  5829  sorpssin  6378  curry1  6670  curry2  6673  tpostpos2  6732  tz7.44-2  6827  tz7.44-3  6828  frfnom  6854  ecinxp  7141  infssuni  7563  elfiun  7602  marypha1lem  7605  unxpwdom  7724  cdainf  8243  ackbij1lem16  8286  fin23lem26  8376  isf34lem7  8430  isf34lem6  8431  fpwwe2lem11  8686  fpwwe2lem13  8688  fpwwe2  8689  uzin  10757  iooval2  11197  limsupgle  12802  limsupgre  12806  bitsinv1  13485  bitsres  13516  bitsuz  13517  2prm  13626  dfphi2  13696  ressbas2  14074  ressinbas  14079  ressress  14080  restid2  14212  resscatc  14814  dprdz  16203  dprdcntz2  16211  lmhmlsp  16744  lspdisj2  16822  ressmplbas2  17143  pmtrmvd  17612  difopn  18112  mretopd  18170  restcld  18250  restopnb  18253  restfpw  18257  neitr  18258  cnrest2  18364  paste  18372  isnrm2  18436  1stccnp  18540  restnlly  18560  lly1stc  18574  kgeni  18584  kgencn3  18605  ptbasfi  18628  hausdiag  18692  qtopval2  18743  qtoprest  18764  filcon  18930  trfil2  18934  trfg  18938  uzrest  18944  trufil  18957  ufileu  18966  fclscf  19072  flimfnfcls  19075  tsmsres  19188  trust  19274  restutopopn  19283  metustfbasOLD  19610  metustfbas  19611  restmetu  19632  xrtgioo  19852  xrsmopn  19858  clsocv  20219  cmetss  20282  ovoliunlem1  20413  difmbl  20452  voliunlem1  20459  volsup2  20512  i1fima  20583  i1fima2  20584  i1fd  20586  itg1addlem5  20605  itg1climres  20619  dvmptid  20858  dvmptc  20859  dvlipcn  20893  dvlip2  20894  dvcnvrelem1  20916  dvcvx  20919  taylthlem1  21304  taylthlem2  21305  psercn  21357  pige3  21445  dvlog  21562  dvcxp1  21646  ppiprm  21955  chtprm  21957  eupares  22718  chm1i  23981  dmdsl3  24841  atssma  24904  dmdbr6ati  24949  imadifxp  25067  fnresin  25075  sspreima  25092  df1stres  25129  df2ndres  25130  xrge0base  25277  xrge00  25278  xrge0slmod  25491  esumnul  25682  esumsn  25695  eulerpartlemgs2  25937  probmeasb  25963  ballotlemfp1  26024  signstres  26127  cvmscld  26308  cvmliftmolem1  26316  dfon2lem4  26752  dfrdg2  26762  sspred  26786  nodense  26983  fvline2  27419  mblfinlem3  27610  mblfinlem4  27611  ftc1anclem6  27652  areacirclem1  27664  topbnd  27699  opnbnd  27700  neibastop1  27760  subspopn  27830  ssbnd  27869  heiborlem3  27894  elrfi  28178  setindtr  28521  fnwe2lem2  28552  lmhmlnmsplit  28588  proot1hash  28750  fgraphopab  28760  dmressnsn  29207  fnresfnco  29211  resisresindm  29320  f0rn0  29322  bnj1322  30664  lcvexchlem3  31384  dihglblem5aN  33640
  Copyright terms: Public domain W3C validator