Definition df-ss 3870

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 28464). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3909). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3872). For a more traditional definition, but requiring a dummy variable, see dfss2 3873. Other possible definitions are given by dfss3 3875, dfss4 4159, sspss 4000, ssequn1 4080, ssequn2 4083, sseqin2 4116, and ssdif0 4264.

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 10702 and 1ex 10794) or ℝ ( cf. df-r 10704 and reex 10785). 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 10785). 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 3853	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3852	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1543	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 209	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3871  ss2abdv  3963  sseqin2  4116  dfss7  4141  inabs  4156  nssinpss  4157  dfrab3ss  4213  disjssun  4368  riinn0  4977  ssex  5199  op1stb  5340  ssdmres  5859  dmressnsn  5878  sspred  6148  ordtri3or  6223  fnimaeq0  6489  f0rn0  6582  fnreseql  6846  cnvimainrn  6865  sspreima  6866  sorpssin  7497  curry1  7850  curry2  7853  tpostpos2  7967  tz7.44-2  8121  tz7.44-3  8122  frfnom  8148  ecinxp  8452  infssuni  8945  elfiun  9024  marypha1lem  9027  unxpwdom  9183  djuinf  9767  ackbij1lem16  9814  fin23lem26  9904  isf34lem7  9958  isf34lem6  9959  fpwwe2lem10  10219  fpwwe2lem12  10221  fpwwe2  10222  uzin  12439  iooval2  12933  limsupgle  15003  limsupgre  15007  bitsinv1  15964  bitsres  15995  bitsuz  15996  2prm  16212  dfphi2  16290  ressbas2  16739  ressinbas  16744  ressval3d  16745  ressress  16746  restid2  16889  resscatc  17569  symgvalstruct  18743  pmtrmvd  18802  dprdz  19371  dprdcntz2  19379  lmhmlsp  20040  lspdisj2  20118  ressmplbas2  20938  difopn  21885  mretopd  21943  restcld  22023  restopnb  22026  restfpw  22030  neitr  22031  cnrest2  22137  paste  22145  isnrm2  22209  1stccnp  22313  restnlly  22333  lly1stc  22347  kgeni  22388  kgencn3  22409  ptbasfi  22432  hausdiag  22496  qtopval2  22547  qtoprest  22568  trfil2  22738  trfg  22742  uzrest  22748  trufil  22761  ufileu  22770  fclscf  22876  flimfnfcls  22879  tsmsres  22995  trust  23081  restutopopn  23090  metustfbas  23409  restmetu  23422  xrtgioo  23657  xrsmopn  23663  clsocv  24101  cmetss  24167  ovoliunlem1  24353  difmbl  24394  voliunlem1  24401  volsup2  24456  i1fima  24529  i1fima2  24530  i1fd  24532  itg1addlem5  24552  itg1climres  24566  dvmptid  24808  dvmptc  24809  dvlipcn  24845  dvlip2  24846  dvcnvrelem1  24868  dvcvx  24871  taylthlem1  25219  taylthlem2  25220  psercn  25272  pige3ALT  25363  dvlog  25493  dvcxp1  25580  ppiprm  25987  chtprm  25989  chm1i  29491  dmdsl3  30350  atssma  30413  dmdbr6ati  30458  imadifxp  30613  fnresin  30634  preimane  30681  fnpreimac  30682  mptprop  30705  df1stres  30710  df2ndres  30711  preiman0  30716  xrge0base  30967  xrge00  30968  gsumhashmul  30989  cycpm2tr  31059  xrge0slmod  31216  fldexttr  31401  zarcmplem  31499  esumnul  31682  esumsnf  31698  baselcarsg  31939  difelcarsg  31943  eulerpartlemgs2  32013  probmeasb  32063  ballotlemfp1  32124  signstres  32220  ftc2re  32244  bnj1322  32469  cvmscld  32902  cvmliftmolem1  32910  mrsubvrs  33151  elmsta  33177  dfon2lem4  33432  dfrdg2  33441  nolesgn2ores  33561  nogesgn1ores  33563  nodense  33581  nosupres  33596  nosupbnd2lem1  33604  noinfres  33611  noinfbnd2lem1  33619  lrrecpred  33787  fvline2  34134  topbnd  34199  opnbnd  34200  neibastop1  34234  bj-disj2r  34904  bj-restsnss2  34939  bj-0int  34956  bj-prmoore  34970  bj-inexeqex  35009  bj-idreseq  35017  mblfinlem3  35502  mblfinlem4  35503  ftc1anclem6  35541  areacirclem1  35551  subspopn  35596  ssbnd  35632  heiborlem3  35657  lcvexchlem3  36736  dihglblem5aN  38992  elrfi  40160  setindtr  40490  fnwe2lem2  40520  lmhmlnmsplit  40556  proot1hash  40669  fgraphopab  40679  iunrelexp0  40928  gneispace  41362  uzinico2  42716  limsupval3  42851  limsupvaluz  42867  liminfval5  42924  fouriersw  43390  saliincl  43484  saldifcl2  43485  gsumge0cl  43527  sge0sn  43535  sge0tsms  43536  sge0split  43565  caragenunidm  43664  fnresfnco  44150  fcoreslem2  44173  imaelsetpreimafv  44463  lidlbas  45097  iscnrm3rlem1  45850  iscnrm3rlem4  45853