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

Definition df-ss 3581
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 27254). Note that 𝐴𝐴 (proved in ssid 3616). Contrast this relationship with the relationship 𝐴𝐵 (as will be defined in df-pss 3583). For a more traditional definition, but requiring a dummy variable, see dfss2 3584. Other possible definitions are given by dfss3 3585, dfss4 3850, sspss 3698, ssequn1 3775, ssequn2 3778, sseqin2 3809, and ssdif0 3933. (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
df-ss (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wss 3567 . 2 wff 𝐴𝐵
41, 2cin 3566 . . 3 class (𝐴𝐵)
54, 1wceq 1481 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 196 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3582  sseqin2  3809  dfss1OLD  3810  inabs  3847  nssinpss  3848  dfrab3ss  3897  disjssun  4027  riinn0  4586  ssex  4793  op1stb  4931  ssdmres  5408  resima2OLD  5421  dmressnsn  5426  sspred  5676  ordtri3or  5743  fnimaeq0  6000  f0rn0  6077  fnreseql  6313  sorpssin  6930  curry1  7254  curry2  7257  tpostpos2  7358  tz7.44-2  7488  tz7.44-3  7489  frfnom  7515  ecinxp  7807  infssuni  8242  elfiun  8321  marypha1lem  8324  unxpwdom  8479  cdainf  8999  ackbij1lem16  9042  fin23lem26  9132  isf34lem7  9186  isf34lem6  9187  fpwwe2lem11  9447  fpwwe2lem13  9449  fpwwe2  9450  uzin  11705  iooval2  12193  limsupgle  14189  limsupgre  14193  bitsinv1  15145  bitsres  15176  bitsuz  15177  2prm  15386  dfphi2  15460  ressbas2  15912  ressinbas  15917  ressval3d  15918  ressress  15919  restid2  16072  resscatc  16736  pmtrmvd  17857  dprdz  18410  dprdcntz2  18418  lmhmlsp  19030  lspdisj2  19108  ressmplbas2  19436  difopn  20819  mretopd  20877  restcld  20957  restopnb  20960  restfpw  20964  neitr  20965  cnrest2  21071  paste  21079  isnrm2  21143  1stccnp  21246  restnlly  21266  lly1stc  21280  kgeni  21321  kgencn3  21342  ptbasfi  21365  hausdiag  21429  qtopval2  21480  qtoprest  21501  trfil2  21672  trfg  21676  uzrest  21682  trufil  21695  ufileu  21704  fclscf  21810  flimfnfcls  21813  tsmsres  21928  trust  22014  restutopopn  22023  metustfbas  22343  restmetu  22356  xrtgioo  22590  xrsmopn  22596  clsocv  23030  cmetss  23094  ovoliunlem1  23251  difmbl  23292  voliunlem1  23299  volsup2  23354  i1fima  23426  i1fima2  23427  i1fd  23429  itg1addlem5  23448  itg1climres  23462  dvmptid  23701  dvmptc  23702  dvlipcn  23738  dvlip2  23739  dvcnvrelem1  23761  dvcvx  23764  taylthlem1  24108  taylthlem2  24109  psercn  24161  pige3  24250  dvlog  24378  dvcxp1  24462  ppiprm  24858  chtprm  24860  chm1i  28285  dmdsl3  29144  atssma  29207  dmdbr6ati  29252  imadifxp  29386  fnresin  29403  sspreima  29420  df1stres  29455  df2ndres  29456  xrge0base  29659  xrge00  29660  xrge0slmod  29818  esumnul  30084  esumsnf  30100  baselcarsg  30342  difelcarsg  30346  eulerpartlemgs2  30416  probmeasb  30466  ballotlemfp1  30527  signstres  30626  ftc2re  30650  bnj1322  30867  cvmscld  31229  cvmliftmolem1  31237  mrsubvrs  31393  elmsta  31419  dfon2lem4  31665  dfrdg2  31675  nolesgn2ores  31799  nodense  31816  nosupres  31827  nosupbnd2lem1  31835  fvline2  32228  topbnd  32294  opnbnd  32295  neibastop1  32329  bj-disj2r  32988  bj-restsnss2  33012  bj-0int  33030  mblfinlem3  33419  mblfinlem4  33420  ftc1anclem6  33461  areacirclem1  33471  subspopn  33519  ssbnd  33558  heiborlem3  33583  lcvexchlem3  34142  dihglblem5aN  36400  elrfi  37076  setindtr  37410  fnwe2lem2  37440  lmhmlnmsplit  37476  proot1hash  37597  fgraphopab  37607  iunrelexp0  37813  gneispace  38252  uzinico2  39592  limsupval3  39724  limsupvaluz  39740  liminfval5  39791  fouriersw  40211  saliincl  40308  saldifcl2  40309  gsumge0cl  40351  sge0sn  40359  sge0tsms  40360  sge0split  40389  caragenunidm  40485  fnresfnco  40969  lidlbas  41688
  Copyright terms: Public domain W3C validator