Definition df-ss 3900

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 28692). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3939). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3902). For a more traditional definition, but requiring a dummy variable, see dfss2 3903. Other possible definitions are given by dfss3 3905, dfss4 4189, sspss 4030, ssequn1 4110, ssequn2 4113, sseqin2 4146, and ssdif0 4294.

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 10810 and 1ex 10902) or ℝ ( cf. df-r 10812 and reex 10893). 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 10893). 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 3883	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3882	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1539	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 205	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3901  ss2abdv  3993  sseqin2  4146  dfss7  4171  inabs  4186  nssinpss  4187  dfrab3ss  4243  disjssun  4398  riinn0  5008  ssex  5240  op1stb  5380  ssdmres  5903  dmressnsn  5922  sspred  6200  ordtri3or  6283  fnimaeq0  6550  f0rn0  6643  fnreseql  6907  cnvimainrn  6926  sspreima  6927  sorpssin  7562  curry1  7915  curry2  7918  tpostpos2  8034  tz7.44-2  8209  tz7.44-3  8210  frfnom  8236  ecinxp  8539  infssuni  9040  elfiun  9119  marypha1lem  9122  unxpwdom  9278  djuinf  9875  ackbij1lem16  9922  fin23lem26  10012  isf34lem7  10066  isf34lem6  10067  fpwwe2lem10  10327  fpwwe2lem12  10329  fpwwe2  10330  uzin  12547  iooval2  13041  limsupgle  15114  limsupgre  15118  bitsinv1  16077  bitsres  16108  bitsuz  16109  2prm  16325  dfphi2  16403  ressbas2  16875  ressinbas  16881  ressval3d  16882  ressval3dOLD  16883  ressress  16884  restid2  17058  resscatc  17740  symgvalstruct  18919  symgvalstructOLD  18920  pmtrmvd  18979  dprdz  19548  dprdcntz2  19556  lmhmlsp  20226  lspdisj2  20304  ressmplbas2  21138  difopn  22093  mretopd  22151  restcld  22231  restopnb  22234  restfpw  22238  neitr  22239  cnrest2  22345  paste  22353  isnrm2  22417  1stccnp  22521  restnlly  22541  lly1stc  22555  kgeni  22596  kgencn3  22617  ptbasfi  22640  hausdiag  22704  qtopval2  22755  qtoprest  22776  trfil2  22946  trfg  22950  uzrest  22956  trufil  22969  ufileu  22978  fclscf  23084  flimfnfcls  23087  tsmsres  23203  trust  23289  restutopopn  23298  metustfbas  23619  restmetu  23632  xrtgioo  23875  xrsmopn  23881  clsocv  24319  cmetss  24385  ovoliunlem1  24571  difmbl  24612  voliunlem1  24619  volsup2  24674  i1fima  24747  i1fima2  24748  i1fd  24750  itg1addlem5  24770  itg1climres  24784  dvmptid  25026  dvmptc  25027  dvlipcn  25063  dvlip2  25064  dvcnvrelem1  25086  dvcvx  25089  taylthlem1  25437  taylthlem2  25438  psercn  25490  pige3ALT  25581  dvlog  25711  dvcxp1  25798  ppiprm  26205  chtprm  26207  chm1i  29719  dmdsl3  30578  atssma  30641  dmdbr6ati  30686  imadifxp  30841  fnresin  30862  preimane  30909  fnpreimac  30910  mptprop  30933  df1stres  30938  df2ndres  30939  preiman0  30944  xrge0base  31196  xrge00  31197  gsumhashmul  31218  cycpm2tr  31288  xrge0slmod  31450  fldexttr  31635  zarcmplem  31733  esumnul  31916  esumsnf  31932  baselcarsg  32173  difelcarsg  32177  eulerpartlemgs2  32247  probmeasb  32297  ballotlemfp1  32358  signstres  32454  ftc2re  32478  bnj1322  32702  cvmscld  33135  cvmliftmolem1  33143  mrsubvrs  33384  elmsta  33410  dfon2lem4  33668  dfrdg2  33677  nolesgn2ores  33802  nogesgn1ores  33804  nodense  33822  nosupres  33837  nosupbnd2lem1  33845  noinfres  33852  noinfbnd2lem1  33860  lrrecpred  34028  fvline2  34375  topbnd  34440  opnbnd  34441  neibastop1  34475  bj-disj2r  35145  bj-restsnss2  35182  bj-0int  35199  bj-prmoore  35213  bj-inexeqex  35252  bj-idreseq  35260  mblfinlem3  35743  mblfinlem4  35744  ftc1anclem6  35782  areacirclem1  35792  subspopn  35837  ssbnd  35873  heiborlem3  35898  lcvexchlem3  36977  dihglblem5aN  39233  elrfi  40432  setindtr  40762  fnwe2lem2  40792  lmhmlnmsplit  40828  proot1hash  40941  fgraphopab  40951  iunrelexp0  41199  gneispace  41633  uzinico2  42990  limsupval3  43123  limsupvaluz  43139  liminfval5  43196  fouriersw  43662  saliincl  43756  saldifcl2  43757  gsumge0cl  43799  sge0sn  43807  sge0tsms  43808  sge0split  43837  caragenunidm  43936  fnresfnco  44422  fcoreslem2  44445  imaelsetpreimafv  44735  lidlbas  45369  iscnrm3rlem1  46122  iscnrm3rlem4  46125