Definition df-ss 3880

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 27894). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3916). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3882). For a more traditional definition, but requiring a dummy variable, see dfss2 3883. Other possible definitions are given by dfss3 3884, dfss4 4161, sspss 4003, ssequn1 4083, ssequn2 4086, sseqin2 4118, and ssdif0 4249.

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 10398 and 1ex 10490) or ℝ ( cf. df-r 10400 and reex 10481). 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 10481). 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 3865	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3864	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1525	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 207	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3881  sseqin2  4118  dfss7  4143  inabs  4158  nssinpss  4159  dfrab3ss  4207  disjssun  4337  riinn0  4910  ssex  5123  op1stb  5262  ssdmres  5764  dmressnsn  5782  sspred  6038  ordtri3or  6105  fnimaeq0  6356  f0rn0  6439  fnreseql  6690  sorpssin  7322  curry1  7662  curry2  7665  tpostpos2  7771  tz7.44-2  7902  tz7.44-3  7903  frfnom  7929  ecinxp  8229  infssuni  8668  elfiun  8747  marypha1lem  8750  unxpwdom  8906  djuinf  9467  ackbij1lem16  9510  fin23lem26  9600  isf34lem7  9654  isf34lem6  9655  fpwwe2lem11  9915  fpwwe2lem13  9917  fpwwe2  9918  uzin  12131  iooval2  12625  limsupgle  14672  limsupgre  14676  bitsinv1  15628  bitsres  15659  bitsuz  15660  2prm  15869  dfphi2  15944  ressbas2  16388  ressinbas  16393  ressval3d  16394  ressress  16395  restid2  16537  resscatc  17198  pmtrmvd  18319  dprdz  18873  dprdcntz2  18881  lmhmlsp  19515  lspdisj2  19593  ressmplbas2  19927  difopn  21330  mretopd  21388  restcld  21468  restopnb  21471  restfpw  21475  neitr  21476  cnrest2  21582  paste  21590  isnrm2  21654  1stccnp  21758  restnlly  21778  lly1stc  21792  kgeni  21833  kgencn3  21854  ptbasfi  21877  hausdiag  21941  qtopval2  21992  qtoprest  22013  trfil2  22183  trfg  22187  uzrest  22193  trufil  22206  ufileu  22215  fclscf  22321  flimfnfcls  22324  tsmsres  22439  trust  22525  restutopopn  22534  metustfbas  22854  restmetu  22867  xrtgioo  23101  xrsmopn  23107  clsocv  23540  cmetss  23606  ovoliunlem1  23790  difmbl  23831  voliunlem1  23838  volsup2  23893  i1fima  23966  i1fima2  23967  i1fd  23969  itg1addlem5  23988  itg1climres  24002  dvmptid  24241  dvmptc  24242  dvlipcn  24278  dvlip2  24279  dvcnvrelem1  24301  dvcvx  24304  taylthlem1  24648  taylthlem2  24649  psercn  24701  pige3ALT  24792  dvlog  24919  dvcxp1  25006  ppiprm  25414  chtprm  25416  chm1i  28920  dmdsl3  29779  atssma  29842  dmdbr6ati  29887  imadifxp  30037  fnresin  30057  sspreima  30078  preimane  30101  fnpreimac  30102  mptprop  30118  df1stres  30123  df2ndres  30124  xrge0base  30342  xrge00  30343  cycpm2tr  30404  xrge0slmod  30567  fldexttr  30648  esumnul  30920  esumsnf  30936  baselcarsg  31177  difelcarsg  31181  eulerpartlemgs2  31251  probmeasb  31301  ballotlemfp1  31362  signstres  31458  ftc2re  31482  bnj1322  31707  cvmscld  32130  cvmliftmolem1  32138  mrsubvrs  32379  elmsta  32405  dfon2lem4  32641  dfrdg2  32651  nolesgn2ores  32790  nodense  32807  nosupres  32818  nosupbnd2lem1  32826  fvline2  33218  topbnd  33283  opnbnd  33284  neibastop1  33318  bj-disj2r  33963  bj-restsnss2  33995  bj-0int  34013  mblfinlem3  34483  mblfinlem4  34484  ftc1anclem6  34524  areacirclem1  34534  subspopn  34580  ssbnd  34619  heiborlem3  34644  lcvexchlem3  35724  dihglblem5aN  37980  elrfi  38797  setindtr  39127  fnwe2lem2  39157  lmhmlnmsplit  39193  proot1hash  39306  fgraphopab  39316  iunrelexp0  39553  gneispace  39990  uzinico2  41401  limsupval3  41536  limsupvaluz  41552  liminfval5  41609  fouriersw  42080  saliincl  42174  saldifcl2  42175  gsumge0cl  42217  sge0sn  42225  sge0tsms  42226  sge0split  42255  caragenunidm  42354  fnresfnco  42814  lidlbas  43694