Definition df-ss 3964

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30250). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4002). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3966). For a more traditional definition, but requiring a dummy variable, see dfss2 3967. Other possible definitions are given by dfss3 3968, dfss4 4259, sspss 4097, ssequn1 4180, ssequn2 4183, sseqin2 4215, and ssdif0 4364.

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 11147 and 1ex 11241) or ℝ ( cf. df-r 11149 and reex 11230). 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 11230). 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 3947	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3946	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1534	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 205	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3965  ss2abdv  4058  sseqin2  4215  dfss7  4241  inabs  4256  nssinpss  4257  dfrab3ss  4313  disjssun  4468  riinn0  5086  ssex  5321  op1stb  5473  ssdmres  6008  dmressnsn  6027  sspred  6314  ordtri3or  6401  fnimaeq0  6688  f0rn0  6782  fnreseql  7057  cnvimainrn  7076  sspreima  7077  sorpssin  7736  curry1  8109  curry2  8112  tpostpos2  8253  tz7.44-2  8428  tz7.44-3  8429  frfnom  8456  ecinxp  8811  infssuni  9368  elfiun  9454  marypha1lem  9457  unxpwdom  9613  djuinf  10212  ackbij1lem16  10259  fin23lem26  10349  isf34lem7  10403  isf34lem6  10404  fpwwe2lem10  10664  fpwwe2lem12  10666  fpwwe2  10667  uzin  12893  iooval2  13390  limsupgle  15454  limsupgre  15458  bitsinv1  16417  bitsres  16448  bitsuz  16449  2prm  16663  dfphi2  16743  ressbas2  17218  ressinbas  17226  ressval3d  17227  ressval3dOLD  17228  ressress  17229  restid2  17412  resscatc  18098  symgvalstruct  19351  symgvalstructOLD  19352  pmtrmvd  19411  dprdz  19987  dprdcntz2  19995  lmhmlsp  20934  lspdisj2  21015  lidlbas  21110  ressmplbas2  21965  psdmullem  22089  difopn  22951  mretopd  23009  restcld  23089  restopnb  23092  restfpw  23096  neitr  23097  cnrest2  23203  paste  23211  isnrm2  23275  1stccnp  23379  restnlly  23399  lly1stc  23413  kgeni  23454  kgencn3  23475  ptbasfi  23498  hausdiag  23562  qtopval2  23613  qtoprest  23634  trfil2  23804  trfg  23808  uzrest  23814  trufil  23827  ufileu  23836  fclscf  23942  flimfnfcls  23945  tsmsres  24061  trust  24147  restutopopn  24156  metustfbas  24479  restmetu  24492  xrtgioo  24735  xrsmopn  24741  clsocv  25191  cmetss  25257  ovoliunlem1  25444  difmbl  25485  voliunlem1  25492  volsup2  25547  i1fima  25620  i1fima2  25621  i1fd  25623  itg1addlem5  25643  itg1climres  25657  dvmptid  25902  dvmptc  25903  dvlipcn  25940  dvlip2  25941  dvcnvrelem1  25963  dvcvx  25966  taylthlem1  26321  taylthlem2  26322  taylthlem2OLD  26323  psercn  26376  pige3ALT  26467  dvlog  26598  dvcxp1  26687  ppiprm  27096  chtprm  27098  nolesgn2ores  27618  nogesgn1ores  27620  nodense  27638  nosupres  27653  nosupbnd2lem1  27661  noinfres  27668  noinfbnd2lem1  27676  lrrecpred  27874  chm1i  31279  dmdsl3  32138  atssma  32201  dmdbr6ati  32246  imadifxp  32404  fnresin  32424  preimane  32469  fnpreimac  32470  mptprop  32491  df1stres  32496  df2ndres  32497  preiman0  32502  xrge0base  32754  xrge00  32755  gsumhashmul  32783  cycpm2tr  32853  xrge0slmod  33073  resssra  33287  fldexttr  33350  zarcmplem  33482  esumnul  33667  esumsnf  33683  baselcarsg  33926  difelcarsg  33930  eulerpartlemgs2  34000  probmeasb  34050  ballotlemfp1  34111  signstres  34207  ftc2re  34230  bnj1322  34453  cvmscld  34883  cvmliftmolem1  34891  mrsubvrs  35132  elmsta  35158  dfon2lem4  35382  dfrdg2  35391  fvline2  35742  topbnd  35808  opnbnd  35809  neibastop1  35843  bj-disj2r  36507  bj-restsnss2  36563  bj-0int  36580  bj-prmoore  36594  bj-inexeqex  36633  bj-idreseq  36641  mblfinlem3  37132  mblfinlem4  37133  ftc1anclem6  37171  areacirclem1  37181  subspopn  37225  ssbnd  37261  heiborlem3  37286  lcvexchlem3  38508  dihglblem5aN  40765  elrfi  42114  setindtr  42445  fnwe2lem2  42475  lmhmlnmsplit  42511  proot1hash  42623  fgraphopab  42631  tfsconcatrev  42777  insucid  42833  iunrelexp0  43132  gneispace  43564  restsubel  44524  uzinico2  44947  limsupval3  45080  limsupvaluz  45096  liminfval5  45153  fouriersw  45619  saliinclf  45714  saldifcl2  45716  gsumge0cl  45759  sge0sn  45767  sge0tsms  45768  sge0split  45797  caragenunidm  45896  fnresfnco  46423  fcoreslem2  46446  imaelsetpreimafv  46735  iscnrm3rlem1  47959  iscnrm3rlem4  47962