Definition df-ss 3958

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30175). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3997). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3960). For a more traditional definition, but requiring a dummy variable, see dfss2 3961. Other possible definitions are given by dfss3 3963, dfss4 4251, sspss 4092, ssequn1 4173, ssequn2 4176, sseqin2 4208, and ssdif0 4356.

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 11209) 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 3941	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3940	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1533	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 205	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3959  ss2abdv  4053  sseqin2  4208  dfss7  4233  inabs  4248  nssinpss  4249  dfrab3ss  4305  disjssun  4460  riinn0  5077  ssex  5312  op1stb  5462  ssdmres  5995  dmressnsn  6014  sspred  6300  ordtri3or  6387  fnimaeq0  6674  f0rn0  6767  fnreseql  7040  cnvimainrn  7059  sspreima  7060  sorpssin  7715  curry1  8085  curry2  8088  tpostpos2  8228  tz7.44-2  8403  tz7.44-3  8404  frfnom  8431  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  12861  iooval2  13358  limsupgle  15423  limsupgre  15427  bitsinv1  16386  bitsres  16417  bitsuz  16418  2prm  16632  dfphi2  16712  ressbas2  17187  ressinbas  17195  ressval3d  17196  ressval3dOLD  17197  ressress  17198  restid2  17381  resscatc  18067  symgvalstruct  19312  symgvalstructOLD  19313  pmtrmvd  19372  dprdz  19948  dprdcntz2  19956  lmhmlsp  20893  lspdisj2  20974  lidlbas  21069  ressmplbas2  21913  difopn  22882  mretopd  22940  restcld  23020  restopnb  23023  restfpw  23027  neitr  23028  cnrest2  23134  paste  23142  isnrm2  23206  1stccnp  23310  restnlly  23330  lly1stc  23344  kgeni  23385  kgencn3  23406  ptbasfi  23429  hausdiag  23493  qtopval2  23544  qtoprest  23565  trfil2  23735  trfg  23739  uzrest  23745  trufil  23758  ufileu  23767  fclscf  23873  flimfnfcls  23876  tsmsres  23992  trust  24078  restutopopn  24087  metustfbas  24410  restmetu  24423  xrtgioo  24666  xrsmopn  24672  clsocv  25122  cmetss  25188  ovoliunlem1  25375  difmbl  25416  voliunlem1  25423  volsup2  25478  i1fima  25551  i1fima2  25552  i1fd  25554  itg1addlem5  25574  itg1climres  25588  dvmptid  25833  dvmptc  25834  dvlipcn  25871  dvlip2  25872  dvcnvrelem1  25894  dvcvx  25897  taylthlem1  26250  taylthlem2  26251  psercn  26304  pige3ALT  26395  dvlog  26526  dvcxp1  26615  ppiprm  27024  chtprm  27026  nolesgn2ores  27546  nogesgn1ores  27548  nodense  27566  nosupres  27581  nosupbnd2lem1  27589  noinfres  27596  noinfbnd2lem1  27604  lrrecpred  27802  chm1i  31204  dmdsl3  32063  atssma  32126  dmdbr6ati  32171  imadifxp  32327  fnresin  32345  preimane  32390  fnpreimac  32391  mptprop  32415  df1stres  32420  df2ndres  32421  preiman0  32426  xrge0base  32677  xrge00  32678  gsumhashmul  32702  cycpm2tr  32772  xrge0slmod  32956  resssra  33182  fldexttr  33245  zarcmplem  33381  esumnul  33566  esumsnf  33582  baselcarsg  33825  difelcarsg  33829  eulerpartlemgs2  33899  probmeasb  33949  ballotlemfp1  34010  signstres  34106  ftc2re  34129  bnj1322  34352  cvmscld  34782  cvmliftmolem1  34790  mrsubvrs  35031  elmsta  35057  dfon2lem4  35281  dfrdg2  35290  fvline2  35641  gg-taylthlem2  35684  topbnd  35710  opnbnd  35711  neibastop1  35745  bj-disj2r  36410  bj-restsnss2  36466  bj-0int  36483  bj-prmoore  36497  bj-inexeqex  36536  bj-idreseq  36544  mblfinlem3  37031  mblfinlem4  37032  ftc1anclem6  37070  areacirclem1  37080  subspopn  37124  ssbnd  37160  heiborlem3  37185  lcvexchlem3  38410  dihglblem5aN  40667  elrfi  41984  setindtr  42315  fnwe2lem2  42345  lmhmlnmsplit  42381  proot1hash  42493  fgraphopab  42502  tfsconcatrev  42648  insucid  42704  iunrelexp0  43003  gneispace  43435  restsubel  44396  uzinico2  44821  limsupval3  44954  limsupvaluz  44970  liminfval5  45027  fouriersw  45493  saliinclf  45588  saldifcl2  45590  gsumge0cl  45633  sge0sn  45641  sge0tsms  45642  sge0split  45671  caragenunidm  45770  fnresfnco  46297  fcoreslem2  46320  imaelsetpreimafv  46609  iscnrm3rlem1  47821  iscnrm3rlem4  47824