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 3951
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 28134). Note that 𝐴𝐴 (proved in ssid 3988). Contrast this relationship with the relationship 𝐴𝐵 (as will be defined in df-pss 3953). For a more traditional definition, but requiring a dummy variable, see dfss2 3954. Other possible definitions are given by dfss3 3955, dfss4 4234, sspss 4075, ssequn1 4155, ssequn2 4158, sseqin2 4191, and ssdif0 4322.

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 10534 and 1ex 10626) or ( cf. df-r 10536 and reex 10617). 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. https://us.metamath.org/downloads/grammar-ambiguity.txt 10617). 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 3935 . 2 wff 𝐴𝐵
41, 2cin 3934 . . 3 class (𝐴𝐵)
54, 1wceq 1528 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 207 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3952  sseqin2  4191  dfss7  4216  inabs  4231  nssinpss  4232  dfrab3ss  4280  disjssun  4415  riinn0  4997  ssex  5217  op1stb  5355  ssdmres  5870  dmressnsn  5888  sspred  6150  ordtri3or  6217  fnimaeq0  6475  f0rn0  6558  fnreseql  6811  sorpssin  7446  curry1  7790  curry2  7793  tpostpos2  7904  tz7.44-2  8034  tz7.44-3  8035  frfnom  8061  ecinxp  8362  infssuni  8804  elfiun  8883  marypha1lem  8886  unxpwdom  9042  djuinf  9603  ackbij1lem16  9646  fin23lem26  9736  isf34lem7  9790  isf34lem6  9791  fpwwe2lem11  10051  fpwwe2lem13  10053  fpwwe2  10054  uzin  12267  iooval2  12761  limsupgle  14824  limsupgre  14828  bitsinv1  15781  bitsres  15812  bitsuz  15813  2prm  16026  dfphi2  16101  ressbas2  16545  ressinbas  16550  ressval3d  16551  ressress  16552  restid2  16694  resscatc  17355  pmtrmvd  18515  dprdz  19083  dprdcntz2  19091  lmhmlsp  19752  lspdisj2  19830  ressmplbas2  20166  difopn  21572  mretopd  21630  restcld  21710  restopnb  21713  restfpw  21717  neitr  21718  cnrest2  21824  paste  21832  isnrm2  21896  1stccnp  22000  restnlly  22020  lly1stc  22034  kgeni  22075  kgencn3  22096  ptbasfi  22119  hausdiag  22183  qtopval2  22234  qtoprest  22255  trfil2  22425  trfg  22429  uzrest  22435  trufil  22448  ufileu  22457  fclscf  22563  flimfnfcls  22566  tsmsres  22681  trust  22767  restutopopn  22776  metustfbas  23096  restmetu  23109  xrtgioo  23343  xrsmopn  23349  clsocv  23782  cmetss  23848  ovoliunlem1  24032  difmbl  24073  voliunlem1  24080  volsup2  24135  i1fima  24208  i1fima2  24209  i1fd  24211  itg1addlem5  24230  itg1climres  24244  dvmptid  24483  dvmptc  24484  dvlipcn  24520  dvlip2  24521  dvcnvrelem1  24543  dvcvx  24546  taylthlem1  24890  taylthlem2  24891  psercn  24943  pige3ALT  25034  dvlog  25161  dvcxp1  25248  ppiprm  25656  chtprm  25658  chm1i  29161  dmdsl3  30020  atssma  30083  dmdbr6ati  30128  imadifxp  30280  fnresin  30300  sspreima  30321  preimane  30344  fnpreimac  30345  mptprop  30361  df1stres  30366  df2ndres  30367  xrge0base  30600  xrge00  30601  cycpm2tr  30689  xrge0slmod  30845  fldexttr  30948  esumnul  31207  esumsnf  31223  baselcarsg  31464  difelcarsg  31468  eulerpartlemgs2  31538  probmeasb  31588  ballotlemfp1  31649  signstres  31745  ftc2re  31769  bnj1322  31994  cvmscld  32418  cvmliftmolem1  32426  mrsubvrs  32667  elmsta  32693  dfon2lem4  32929  dfrdg2  32938  nolesgn2ores  33077  nodense  33094  nosupres  33105  nosupbnd2lem1  33113  fvline2  33505  topbnd  33570  opnbnd  33571  neibastop1  33605  bj-disj2r  34238  bj-restsnss2  34270  bj-0int  34288  bj-inexeqex  34339  bj-idreseq  34347  mblfinlem3  34813  mblfinlem4  34814  ftc1anclem6  34854  areacirclem1  34864  subspopn  34910  ssbnd  34949  heiborlem3  34974  lcvexchlem3  36054  dihglblem5aN  38310  elrfi  39171  setindtr  39501  fnwe2lem2  39531  lmhmlnmsplit  39567  proot1hash  39680  fgraphopab  39690  iunrelexp0  39927  gneispace  40364  uzinico2  41718  limsupval3  41853  limsupvaluz  41869  liminfval5  41926  fouriersw  42397  saliincl  42491  saldifcl2  42492  gsumge0cl  42534  sge0sn  42542  sge0tsms  42543  sge0split  42572  caragenunidm  42671  fnresfnco  43157  lidlbas  44092
  Copyright terms: Public domain W3C validator