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 3721
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 27587). Note that 𝐴𝐴 (proved in ssid 3757). Contrast this relationship with the relationship 𝐴𝐵 (as will be defined in df-pss 3723). For a more traditional definition, but requiring a dummy variable, see dfss2 3724. Other possible definitions are given by dfss3 3725, dfss4 3993, sspss 3840, ssequn1 3918, ssequn2 3921, sseqin2 3952, and ssdif0 4077.

We prefer the label "ss" ("subset") for , despite the fact that it applies to classes. It is much more common to refer to this as the subset relation than subclass, especially since most of the time the arguments are in fact sets (and for pragmatic reasons we don't want to need to use different operations for sets). The way set.mm is set up, many things are technically classes despite morally (and provably) being sets, like 1 (cf. df-1 10128 and 1ex 10219) or ( cf. df-r 10130 and reex 10211) . This has to do with the fact that there are no "set expressions": classes are expressions but there are only set variables in set.mm (cf. http://us.metamath.org/downloads/grammar-ambiguity.txt). This is why we use both for subclass relations and for subset relations and call it "subset". (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 3707 . 2 wff 𝐴𝐵
41, 2cin 3706 . . 3 class (𝐴𝐵)
54, 1wceq 1624 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 196 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3722  sseqin2  3952  dfss1OLD  3953  inabs  3990  nssinpss  3991  dfrab3ss  4040  disjssun  4172  riinn0  4739  ssex  4946  op1stb  5080  ssdmres  5570  resima2OLD  5583  dmressnsn  5588  sspred  5841  ordtri3or  5908  fnimaeq0  6166  f0rn0  6243  fnreseql  6482  sorpssin  7102  curry1  7429  curry2  7432  tpostpos2  7534  tz7.44-2  7664  tz7.44-3  7665  frfnom  7691  ecinxp  7981  infssuni  8414  elfiun  8493  marypha1lem  8496  unxpwdom  8651  cdainf  9198  ackbij1lem16  9241  fin23lem26  9331  isf34lem7  9385  isf34lem6  9386  fpwwe2lem11  9646  fpwwe2lem13  9648  fpwwe2  9649  uzin  11905  iooval2  12393  limsupgle  14399  limsupgre  14403  bitsinv1  15358  bitsres  15389  bitsuz  15390  2prm  15599  dfphi2  15673  ressbas2  16125  ressinbas  16130  ressval3d  16131  ressress  16132  restid2  16285  resscatc  16948  pmtrmvd  18068  dprdz  18621  dprdcntz2  18629  lmhmlsp  19243  lspdisj2  19321  ressmplbas2  19649  difopn  21032  mretopd  21090  restcld  21170  restopnb  21173  restfpw  21177  neitr  21178  cnrest2  21284  paste  21292  isnrm2  21356  1stccnp  21459  restnlly  21479  lly1stc  21493  kgeni  21534  kgencn3  21555  ptbasfi  21578  hausdiag  21642  qtopval2  21693  qtoprest  21714  trfil2  21884  trfg  21888  uzrest  21894  trufil  21907  ufileu  21916  fclscf  22022  flimfnfcls  22025  tsmsres  22140  trust  22226  restutopopn  22235  metustfbas  22555  restmetu  22568  xrtgioo  22802  xrsmopn  22808  clsocv  23241  cmetss  23305  ovoliunlem1  23462  difmbl  23503  voliunlem1  23510  volsup2  23565  i1fima  23636  i1fima2  23637  i1fd  23639  itg1addlem5  23658  itg1climres  23672  dvmptid  23911  dvmptc  23912  dvlipcn  23948  dvlip2  23949  dvcnvrelem1  23971  dvcvx  23974  taylthlem1  24318  taylthlem2  24319  psercn  24371  pige3  24460  dvlog  24588  dvcxp1  24672  ppiprm  25068  chtprm  25070  chm1i  28616  dmdsl3  29475  atssma  29538  dmdbr6ati  29583  imadifxp  29713  fnresin  29731  sspreima  29748  df1stres  29782  df2ndres  29783  xrge0base  29986  xrge00  29987  xrge0slmod  30145  esumnul  30411  esumsnf  30427  baselcarsg  30669  difelcarsg  30673  eulerpartlemgs2  30743  probmeasb  30793  ballotlemfp1  30854  signstres  30953  ftc2re  30977  bnj1322  31192  cvmscld  31554  cvmliftmolem1  31562  mrsubvrs  31718  elmsta  31744  dfon2lem4  31988  dfrdg2  31998  nolesgn2ores  32123  nodense  32140  nosupres  32151  nosupbnd2lem1  32159  fvline2  32551  topbnd  32617  opnbnd  32618  neibastop1  32652  bj-disj2r  33311  bj-restsnss2  33335  bj-0int  33353  mblfinlem3  33753  mblfinlem4  33754  ftc1anclem6  33795  areacirclem1  33805  subspopn  33853  ssbnd  33892  heiborlem3  33917  lcvexchlem3  34818  dihglblem5aN  37075  elrfi  37751  setindtr  38085  fnwe2lem2  38115  lmhmlnmsplit  38151  proot1hash  38272  fgraphopab  38282  iunrelexp0  38488  gneispace  38926  uzinico2  40284  limsupval3  40419  limsupvaluz  40435  liminfval5  40492  fouriersw  40943  saliincl  41040  saldifcl2  41041  gsumge0cl  41083  sge0sn  41091  sge0tsms  41092  sge0split  41121  caragenunidm  41220  fnresfnco  41704  lidlbas  42425
  Copyright terms: Public domain W3C validator