Definition df-ss 3952

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 28206). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3989). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3954). For a more traditional definition, but requiring a dummy variable, see dfss2 3955. Other possible definitions are given by dfss3 3956, dfss4 4235, sspss 4076, ssequn1 4156, ssequn2 4159, sseqin2 4192, and ssdif0 4323.

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 10545 and 1ex 10637) or ℝ ( cf. df-r 10547 and reex 10628). 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 10628). 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 3936	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3935	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1537	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 208	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3953  sseqin2  4192  dfss7  4217  inabs  4232  nssinpss  4233  dfrab3ss  4281  disjssun  4417  riinn0  5005  ssex  5225  op1stb  5363  ssdmres  5876  dmressnsn  5894  sspred  6156  ordtri3or  6223  fnimaeq0  6481  f0rn0  6564  fnreseql  6818  sorpssin  7457  curry1  7799  curry2  7802  tpostpos2  7913  tz7.44-2  8043  tz7.44-3  8044  frfnom  8070  ecinxp  8372  infssuni  8815  elfiun  8894  marypha1lem  8897  unxpwdom  9053  djuinf  9614  ackbij1lem16  9657  fin23lem26  9747  isf34lem7  9801  isf34lem6  9802  fpwwe2lem11  10062  fpwwe2lem13  10064  fpwwe2  10065  uzin  12279  iooval2  12772  limsupgle  14834  limsupgre  14838  bitsinv1  15791  bitsres  15822  bitsuz  15823  2prm  16036  dfphi2  16111  ressbas2  16555  ressinbas  16560  ressval3d  16561  ressress  16562  restid2  16704  resscatc  17365  symgvalstruct  18525  pmtrmvd  18584  dprdz  19152  dprdcntz2  19160  lmhmlsp  19821  lspdisj2  19899  ressmplbas2  20236  difopn  21642  mretopd  21700  restcld  21780  restopnb  21783  restfpw  21787  neitr  21788  cnrest2  21894  paste  21902  isnrm2  21966  1stccnp  22070  restnlly  22090  lly1stc  22104  kgeni  22145  kgencn3  22166  ptbasfi  22189  hausdiag  22253  qtopval2  22304  qtoprest  22325  trfil2  22495  trfg  22499  uzrest  22505  trufil  22518  ufileu  22527  fclscf  22633  flimfnfcls  22636  tsmsres  22752  trust  22838  restutopopn  22847  metustfbas  23167  restmetu  23180  xrtgioo  23414  xrsmopn  23420  clsocv  23853  cmetss  23919  ovoliunlem1  24103  difmbl  24144  voliunlem1  24151  volsup2  24206  i1fima  24279  i1fima2  24280  i1fd  24282  itg1addlem5  24301  itg1climres  24315  dvmptid  24554  dvmptc  24555  dvlipcn  24591  dvlip2  24592  dvcnvrelem1  24614  dvcvx  24617  taylthlem1  24961  taylthlem2  24962  psercn  25014  pige3ALT  25105  dvlog  25234  dvcxp1  25321  ppiprm  25728  chtprm  25730  chm1i  29233  dmdsl3  30092  atssma  30155  dmdbr6ati  30200  imadifxp  30351  fnresin  30371  sspreima  30392  preimane  30415  fnpreimac  30416  mptprop  30434  df1stres  30439  df2ndres  30440  xrge0base  30672  xrge00  30673  cycpm2tr  30761  xrge0slmod  30917  fldexttr  31048  esumnul  31307  esumsnf  31323  baselcarsg  31564  difelcarsg  31568  eulerpartlemgs2  31638  probmeasb  31688  ballotlemfp1  31749  signstres  31845  ftc2re  31869  bnj1322  32094  cvmscld  32520  cvmliftmolem1  32528  mrsubvrs  32769  elmsta  32795  dfon2lem4  33031  dfrdg2  33040  nolesgn2ores  33179  nodense  33196  nosupres  33207  nosupbnd2lem1  33215  fvline2  33607  topbnd  33672  opnbnd  33673  neibastop1  33707  bj-disj2r  34343  bj-restsnss2  34378  bj-0int  34396  bj-prmoore  34410  bj-inexeqex  34449  bj-idreseq  34457  mblfinlem3  34946  mblfinlem4  34947  ftc1anclem6  34987  areacirclem1  34997  subspopn  35042  ssbnd  35081  heiborlem3  35106  lcvexchlem3  36187  dihglblem5aN  38443  elrfi  39340  setindtr  39670  fnwe2lem2  39700  lmhmlnmsplit  39736  proot1hash  39849  fgraphopab  39859  iunrelexp0  40096  gneispace  40533  uzinico2  41887  limsupval3  42022  limsupvaluz  42038  liminfval5  42095  fouriersw  42565  saliincl  42659  saldifcl2  42660  gsumge0cl  42702  sge0sn  42710  sge0tsms  42711  sge0split  42740  caragenunidm  42839  fnresfnco  43325  imaelsetpreimafv  43604  lidlbas  44243