Definition df-ss 3905

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 28800). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3944). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3907). For a more traditional definition, but requiring a dummy variable, see dfss2 3908. Other possible definitions are given by dfss3 3910, dfss4 4193, sspss 4035, ssequn1 4115, ssequn2 4118, sseqin2 4150, and ssdif0 4298.

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 10888 and 1ex 10980) or ℝ ( cf. df-r 10890 and reex 10971). 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 10971). 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 3888	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3887	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1539	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 205	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3906  ss2abdv  3998  sseqin2  4150  dfss7  4175  inabs  4190  nssinpss  4191  dfrab3ss  4247  disjssun  4402  riinn0  5013  ssex  5246  op1stb  5387  ssdmres  5917  dmressnsn  5936  sspred  6215  ordtri3or  6302  fnimaeq0  6575  f0rn0  6668  fnreseql  6934  cnvimainrn  6953  sspreima  6954  sorpssin  7593  curry1  7953  curry2  7956  tpostpos2  8072  tz7.44-2  8247  tz7.44-3  8248  frfnom  8275  ecinxp  8590  infssuni  9119  elfiun  9198  marypha1lem  9201  unxpwdom  9357  djuinf  9953  ackbij1lem16  10000  fin23lem26  10090  isf34lem7  10144  isf34lem6  10145  fpwwe2lem10  10405  fpwwe2lem12  10407  fpwwe2  10408  uzin  12627  iooval2  13121  limsupgle  15195  limsupgre  15199  bitsinv1  16158  bitsres  16189  bitsuz  16190  2prm  16406  dfphi2  16484  ressbas2  16958  ressinbas  16964  ressval3d  16965  ressval3dOLD  16966  ressress  16967  restid2  17150  resscatc  17833  symgvalstruct  19013  symgvalstructOLD  19014  pmtrmvd  19073  dprdz  19642  dprdcntz2  19650  lmhmlsp  20320  lspdisj2  20398  ressmplbas2  21237  difopn  22194  mretopd  22252  restcld  22332  restopnb  22335  restfpw  22339  neitr  22340  cnrest2  22446  paste  22454  isnrm2  22518  1stccnp  22622  restnlly  22642  lly1stc  22656  kgeni  22697  kgencn3  22718  ptbasfi  22741  hausdiag  22805  qtopval2  22856  qtoprest  22877  trfil2  23047  trfg  23051  uzrest  23057  trufil  23070  ufileu  23079  fclscf  23185  flimfnfcls  23188  tsmsres  23304  trust  23390  restutopopn  23399  metustfbas  23722  restmetu  23735  xrtgioo  23978  xrsmopn  23984  clsocv  24423  cmetss  24489  ovoliunlem1  24675  difmbl  24716  voliunlem1  24723  volsup2  24778  i1fima  24851  i1fima2  24852  i1fd  24854  itg1addlem5  24874  itg1climres  24888  dvmptid  25130  dvmptc  25131  dvlipcn  25167  dvlip2  25168  dvcnvrelem1  25190  dvcvx  25193  taylthlem1  25541  taylthlem2  25542  psercn  25594  pige3ALT  25685  dvlog  25815  dvcxp1  25902  ppiprm  26309  chtprm  26311  chm1i  29827  dmdsl3  30686  atssma  30749  dmdbr6ati  30794  imadifxp  30949  fnresin  30970  preimane  31016  fnpreimac  31017  mptprop  31040  df1stres  31045  df2ndres  31046  preiman0  31051  xrge0base  31303  xrge00  31304  gsumhashmul  31325  cycpm2tr  31395  xrge0slmod  31557  fldexttr  31742  zarcmplem  31840  esumnul  32025  esumsnf  32041  baselcarsg  32282  difelcarsg  32286  eulerpartlemgs2  32356  probmeasb  32406  ballotlemfp1  32467  signstres  32563  ftc2re  32587  bnj1322  32811  cvmscld  33244  cvmliftmolem1  33252  mrsubvrs  33493  elmsta  33519  dfon2lem4  33771  dfrdg2  33780  nolesgn2ores  33884  nogesgn1ores  33886  nodense  33904  nosupres  33919  nosupbnd2lem1  33927  noinfres  33934  noinfbnd2lem1  33942  lrrecpred  34110  fvline2  34457  topbnd  34522  opnbnd  34523  neibastop1  34557  bj-disj2r  35227  bj-restsnss2  35264  bj-0int  35281  bj-prmoore  35295  bj-inexeqex  35334  bj-idreseq  35342  mblfinlem3  35825  mblfinlem4  35826  ftc1anclem6  35864  areacirclem1  35874  subspopn  35919  ssbnd  35955  heiborlem3  35980  lcvexchlem3  37057  dihglblem5aN  39313  elrfi  40523  setindtr  40853  fnwe2lem2  40883  lmhmlnmsplit  40919  proot1hash  41032  fgraphopab  41042  iunrelexp0  41317  gneispace  41751  uzinico2  43107  limsupval3  43240  limsupvaluz  43256  liminfval5  43313  fouriersw  43779  saliincl  43873  saldifcl2  43874  gsumge0cl  43916  sge0sn  43924  sge0tsms  43925  sge0split  43954  caragenunidm  44053  fnresfnco  44546  fcoreslem2  44569  imaelsetpreimafv  44858  lidlbas  45492  iscnrm3rlem1  46245  iscnrm3rlem4  46248