Definition df-ss 3915

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 29080). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3954). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3917). For a more traditional definition, but requiring a dummy variable, see dfss2 3918. Other possible definitions are given by dfss3 3920, dfss4 4206, sspss 4047, ssequn1 4128, ssequn2 4131, sseqin2 4163, and ssdif0 4311.

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 10981 and 1ex 11073) or ℝ ( cf. df-r 10983 and reex 11064). 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 11064). 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 3898	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3897	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1540	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 205	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3916  ss2abdv  4008  sseqin2  4163  dfss7  4188  inabs  4203  nssinpss  4204  dfrab3ss  4260  disjssun  4415  riinn0  5031  ssex  5266  op1stb  5417  ssdmres  5947  dmressnsn  5966  sspred  6248  ordtri3or  6335  fnimaeq0  6618  f0rn0  6711  fnreseql  6982  cnvimainrn  7001  sspreima  7002  sorpssin  7647  curry1  8013  curry2  8016  tpostpos2  8134  tz7.44-2  8309  tz7.44-3  8310  frfnom  8337  ecinxp  8653  infssuni  9209  elfiun  9288  marypha1lem  9291  unxpwdom  9447  djuinf  10046  ackbij1lem16  10093  fin23lem26  10183  isf34lem7  10237  isf34lem6  10238  fpwwe2lem10  10498  fpwwe2lem12  10500  fpwwe2  10501  uzin  12720  iooval2  13214  limsupgle  15286  limsupgre  15290  bitsinv1  16249  bitsres  16280  bitsuz  16281  2prm  16495  dfphi2  16573  ressbas2  17047  ressinbas  17053  ressval3d  17054  ressval3dOLD  17055  ressress  17056  restid2  17239  resscatc  17922  symgvalstruct  19101  symgvalstructOLD  19102  pmtrmvd  19161  dprdz  19729  dprdcntz2  19737  lmhmlsp  20418  lspdisj2  20496  ressmplbas2  21335  difopn  22292  mretopd  22350  restcld  22430  restopnb  22433  restfpw  22437  neitr  22438  cnrest2  22544  paste  22552  isnrm2  22616  1stccnp  22720  restnlly  22740  lly1stc  22754  kgeni  22795  kgencn3  22816  ptbasfi  22839  hausdiag  22903  qtopval2  22954  qtoprest  22975  trfil2  23145  trfg  23149  uzrest  23155  trufil  23168  ufileu  23177  fclscf  23283  flimfnfcls  23286  tsmsres  23402  trust  23488  restutopopn  23497  metustfbas  23820  restmetu  23833  xrtgioo  24076  xrsmopn  24082  clsocv  24521  cmetss  24587  ovoliunlem1  24773  difmbl  24814  voliunlem1  24821  volsup2  24876  i1fima  24949  i1fima2  24950  i1fd  24952  itg1addlem5  24972  itg1climres  24986  dvmptid  25228  dvmptc  25229  dvlipcn  25265  dvlip2  25266  dvcnvrelem1  25288  dvcvx  25291  taylthlem1  25639  taylthlem2  25640  psercn  25692  pige3ALT  25783  dvlog  25913  dvcxp1  26000  ppiprm  26407  chtprm  26409  nolesgn2ores  26927  nogesgn1ores  26929  nodense  26947  nosupres  26962  nosupbnd2lem1  26970  noinfres  26977  noinfbnd2lem1  26985  chm1i  30107  dmdsl3  30966  atssma  31029  dmdbr6ati  31074  imadifxp  31227  fnresin  31248  preimane  31294  fnpreimac  31295  mptprop  31318  df1stres  31323  df2ndres  31324  preiman0  31329  xrge0base  31581  xrge00  31582  gsumhashmul  31603  cycpm2tr  31673  xrge0slmod  31844  fldexttr  32031  zarcmplem  32129  esumnul  32314  esumsnf  32330  baselcarsg  32573  difelcarsg  32577  eulerpartlemgs2  32647  probmeasb  32697  ballotlemfp1  32758  signstres  32854  ftc2re  32878  bnj1322  33101  cvmscld  33534  cvmliftmolem1  33542  mrsubvrs  33783  elmsta  33809  dfon2lem4  34047  dfrdg2  34056  lrrecpred  34211  fvline2  34587  topbnd  34652  opnbnd  34653  neibastop1  34687  bj-disj2r  35355  bj-restsnss2  35411  bj-0int  35428  bj-prmoore  35442  bj-inexeqex  35481  bj-idreseq  35489  mblfinlem3  35972  mblfinlem4  35973  ftc1anclem6  36011  areacirclem1  36021  subspopn  36066  ssbnd  36102  heiborlem3  36127  lcvexchlem3  37354  dihglblem5aN  39611  elrfi  40829  setindtr  41160  fnwe2lem2  41190  lmhmlnmsplit  41226  proot1hash  41339  fgraphopab  41349  iunrelexp0  41683  gneispace  42117  restsubel  43080  uzinico2  43488  limsupval3  43621  limsupvaluz  43637  liminfval5  43694  fouriersw  44160  saliincl  44254  saldifcl2  44255  gsumge0cl  44298  sge0sn  44306  sge0tsms  44307  sge0split  44336  caragenunidm  44435  fnresfnco  44953  fcoreslem2  44976  imaelsetpreimafv  45265  lidlbas  45899  iscnrm3rlem1  46652  iscnrm3rlem4  46655