Definition df-ss 3965

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 29670). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4004). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3967). For a more traditional definition, but requiring a dummy variable, see dfss2 3968. Other possible definitions are given by dfss3 3970, dfss4 4258, sspss 4099, ssequn1 4180, ssequn2 4183, sseqin2 4215, and ssdif0 4363.

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 11115 and 1ex 11207) or ℝ ( cf. df-r 11117 and reex 11198). 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 11198). 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wss 3948	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3947	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1542	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 205	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3966  ss2abdv  4060  sseqin2  4215  dfss7  4240  inabs  4255  nssinpss  4256  dfrab3ss  4312  disjssun  4467  riinn0  5086  ssex  5321  op1stb  5471  ssdmres  6003  dmressnsn  6022  sspred  6307  ordtri3or  6394  fnimaeq0  6681  f0rn0  6774  fnreseql  7047  cnvimainrn  7066  sspreima  7067  sorpssin  7718  curry1  8087  curry2  8090  tpostpos2  8229  tz7.44-2  8404  tz7.44-3  8405  frfnom  8432  ecinxp  8783  infssuni  9340  elfiun  9422  marypha1lem  9425  unxpwdom  9581  djuinf  10180  ackbij1lem16  10227  fin23lem26  10317  isf34lem7  10371  isf34lem6  10372  fpwwe2lem10  10632  fpwwe2lem12  10634  fpwwe2  10635  uzin  12859  iooval2  13354  limsupgle  15418  limsupgre  15422  bitsinv1  16380  bitsres  16411  bitsuz  16412  2prm  16626  dfphi2  16704  ressbas2  17179  ressinbas  17187  ressval3d  17188  ressval3dOLD  17189  ressress  17190  restid2  17373  resscatc  18056  symgvalstruct  19259  symgvalstructOLD  19260  pmtrmvd  19319  dprdz  19895  dprdcntz2  19903  lmhmlsp  20653  lspdisj2  20733  ressmplbas2  21574  difopn  22530  mretopd  22588  restcld  22668  restopnb  22671  restfpw  22675  neitr  22676  cnrest2  22782  paste  22790  isnrm2  22854  1stccnp  22958  restnlly  22978  lly1stc  22992  kgeni  23033  kgencn3  23054  ptbasfi  23077  hausdiag  23141  qtopval2  23192  qtoprest  23213  trfil2  23383  trfg  23387  uzrest  23393  trufil  23406  ufileu  23415  fclscf  23521  flimfnfcls  23524  tsmsres  23640  trust  23726  restutopopn  23735  metustfbas  24058  restmetu  24071  xrtgioo  24314  xrsmopn  24320  clsocv  24759  cmetss  24825  ovoliunlem1  25011  difmbl  25052  voliunlem1  25059  volsup2  25114  i1fima  25187  i1fima2  25188  i1fd  25190  itg1addlem5  25210  itg1climres  25224  dvmptid  25466  dvmptc  25467  dvlipcn  25503  dvlip2  25504  dvcnvrelem1  25526  dvcvx  25529  taylthlem1  25877  taylthlem2  25878  psercn  25930  pige3ALT  26021  dvlog  26151  dvcxp1  26238  ppiprm  26645  chtprm  26647  nolesgn2ores  27165  nogesgn1ores  27167  nodense  27185  nosupres  27200  nosupbnd2lem1  27208  noinfres  27215  noinfbnd2lem1  27223  lrrecpred  27418  chm1i  30697  dmdsl3  31556  atssma  31619  dmdbr6ati  31664  imadifxp  31820  fnresin  31838  preimane  31883  fnpreimac  31884  mptprop  31908  df1stres  31913  df2ndres  31914  preiman0  31919  xrge0base  32174  xrge00  32175  gsumhashmul  32196  cycpm2tr  32266  xrge0slmod  32452  fldexttr  32726  zarcmplem  32850  esumnul  33035  esumsnf  33051  baselcarsg  33294  difelcarsg  33298  eulerpartlemgs2  33368  probmeasb  33418  ballotlemfp1  33479  signstres  33575  ftc2re  33599  bnj1322  33822  cvmscld  34253  cvmliftmolem1  34261  mrsubvrs  34502  elmsta  34528  dfon2lem4  34747  dfrdg2  34756  fvline2  35107  topbnd  35198  opnbnd  35199  neibastop1  35233  bj-disj2r  35898  bj-restsnss2  35954  bj-0int  35971  bj-prmoore  35985  bj-inexeqex  36024  bj-idreseq  36032  mblfinlem3  36516  mblfinlem4  36517  ftc1anclem6  36555  areacirclem1  36565  subspopn  36609  ssbnd  36645  heiborlem3  36670  lcvexchlem3  37895  dihglblem5aN  40152  elrfi  41418  setindtr  41749  fnwe2lem2  41779  lmhmlnmsplit  41815  proot1hash  41928  fgraphopab  41938  tfsconcatrev  42084  insucid  42140  iunrelexp0  42439  gneispace  42871  restsubel  43833  uzinico2  44262  limsupval3  44395  limsupvaluz  44411  liminfval5  44468  fouriersw  44934  saliinclf  45029  saldifcl2  45031  gsumge0cl  45074  sge0sn  45082  sge0tsms  45083  sge0split  45112  caragenunidm  45211  fnresfnco  45738  fcoreslem2  45761  imaelsetpreimafv  46050  lidlbas  46738  iscnrm3rlem1  47527  iscnrm3rlem4  47530