Definition df-ss 3964

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30360). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4002). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3967). For an alternative definition, not requiring a dummy variable, see dfss2 3965. Other possible definitions are given by dfss3 3968, dfss4 4260, sspss 4098, ssequn1 4181, ssequn2 4184, sseqin2 4216, and ssdif0 4366.

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 11166 and 1ex 11260) or ℝ ( cf. df-r 11168 and reex 11249). 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 11249). This is why we use ⊆ both for subclass relations and for subset relations and call it "subset". (Contributed by NM, 8-Jan-2002.) Revised from the original definition dfss2 3965. (Revised by GG, 15-May-2025.)

Assertion

Ref	Expression
df-ss	⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

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		vx	. . . . . 6 setvar 𝑥
5	4	cv 1533	. . . . 5 class 𝑥
6	5, 1	wcel 2099	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2099	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
9	8, 4	wal 1532	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 205	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3965  dfss3  3968  dfss6  3969  dfssf  3970  ssel  3973  ssriv  3983  ssrdv  3985  sstr2  3986  sstr2OLD  3987  eqss  3995  nss  4044  ssralv  4048  ssrexv  4049  rabss2  4074  ssconb  4137  ssequn1  4181  unss  4185  ssin  4232  ssdif0  4366  difin0ss  4373  inssdif0  4374  reldisj  4456  reldisjOLD  4457  ssundif  4492  sbcssg  4528  pwss  4630  snssb  4791  snssgOLD  4793  pwpw0  4822  ssuni  4940  unissb  4947  unissbOLD  4948  iunssf  5052  iunss  5053  dftr2  5272  axpweq  5354  axpow2  5371  ssextss  5459  ssrel  5788  ssrelOLD  5789  ssrel2  5791  ssrelrel  5802  reliun  5822  relop  5857  idrefALT  6123  funimass4  6967  dfom2  7878  inf2  9666  grothprim  10877  psslinpr  11074  ltaddpr  11077  isprm2  16683  vdwmc2  16981  acsmapd  18579  ismhp3  22137  dfconn2  23414  iskgen3  23544  metcld  25325  metcld2  25326  isch2  31156  pjnormssi  32101  ssiun3  32479  ssrelf  32535  bnj1361  34673  bnj978  34794  fineqvpow  34932  dffr5  35576  brsset  35713  sscoid  35737  relowlpssretop  37071  fvineqsneq  37119  unielss  42883  rp-fakeinunass  43182  rababg  43241  dfhe3  43442  snhesn  43453  dffrege76  43606  ntrneiiso  43758  ntrneik2  43759  ntrneix2  43760  ntrneikb  43761  expanduniss  43967  ismnuprim  43968  ismnushort  43975  onfrALTlem2  44222  trsspwALT  44494  trsspwALT2  44495  snssiALTVD  44503  snssiALT  44504  sstrALT2VD  44510  sstrALT2  44511  sbcssgVD  44559  onfrALTlem2VD  44565  sspwimp  44594  sspwimpVD  44595  sspwimpcf  44596  sspwimpcfVD  44597  sspwimpALT  44601  unisnALT  44602  icccncfext  45508