Definition df-ss 3979

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30455). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4017). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3982). For an alternative definition, not requiring a dummy variable, see dfss2 3980. Other possible definitions are given by dfss3 3983, dfss4 4274, sspss 4111, ssequn1 4195, ssequn2 4198, sseqin2 4230, and ssdif0 4371.

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 11160 and 1ex 11254) or ℝ ( cf. df-r 11162 and reex 11243). 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 11243). 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 3980. (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 3962	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1535	. . . . 5 class 𝑥
6	5, 1	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
9	8, 4	wal 1534	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 206	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3980  dfss3  3983  dfss6  3984  dfssf  3985  ssel  3988  ssriv  3998  ssrdv  4000  sstr2  4001  sstr2OLD  4002  eqss  4010  nss  4059  ssralv  4063  ssrexv  4064  rabss2  4087  ssconb  4151  ssequn1  4195  unss  4199  ssin  4246  ssdif0  4371  difin0ss  4378  inssdif0  4379  reldisj  4458  ssundif  4493  sbcssg  4525  pwss  4627  snssb  4786  snssgOLD  4788  pwpw0  4817  ssuni  4936  unissb  4943  unissbOLD  4944  iunssf  5048  iunss  5049  dftr2  5266  axpweq  5356  axpow2  5372  ssextss  5463  ssrel  5794  ssrelOLD  5795  ssrel2  5797  ssrelrel  5808  reliun  5828  relop  5863  idrefALT  6133  funimass4  6972  dfom2  7888  inf2  9660  grothprim  10871  psslinpr  11068  ltaddpr  11071  isprm2  16715  vdwmc2  17012  acsmapd  18611  ismhp3  22163  dfconn2  23442  iskgen3  23572  metcld  25353  metcld2  25354  isch2  31251  pjnormssi  32196  ssiun3  32578  ssrelf  32634  bnj1361  34820  bnj978  34941  fineqvpow  35088  dffr5  35733  brsset  35870  sscoid  35894  ss-ax8  36207  relowlpssretop  37346  fvineqsneq  37394  unielss  43206  rp-fakeinunass  43504  rababg  43563  dfhe3  43764  snhesn  43775  dffrege76  43928  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  expanduniss  44288  ismnuprim  44289  ismnushort  44296  onfrALTlem2  44543  trsspwALT  44815  trsspwALT2  44816  snssiALTVD  44824  snssiALT  44825  sstrALT2VD  44831  sstrALT2  44832  sbcssgVD  44880  onfrALTlem2VD  44886  sspwimp  44915  sspwimpVD  44916  sspwimpcf  44917  sspwimpcfVD  44918  sspwimpALT  44922  unisnALT  44923  ssclaxsep  44946  icccncfext  45842