Definition df-ss 3968

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30446). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4006). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3971). For an alternative definition, not requiring a dummy variable, see dfss2 3969. Other possible definitions are given by dfss3 3972, dfss4 4269, sspss 4102, ssequn1 4186, ssequn2 4189, sseqin2 4223, 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 11163 and 1ex 11257) or ℝ ( cf. df-r 11165 and reex 11246). 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 11246). 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 3969. (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 3951	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1539	. . . . 5 class 𝑥
6	5, 1	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
9	8, 4	wal 1538	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 206	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3969  dfss3  3972  dfss6  3973  dfssf  3974  ssel  3977  ssriv  3987  ssrdv  3989  sstr2  3990  sstr2OLD  3991  eqss  3999  nss  4048  ssralv  4052  ssrexv  4053  ralss  4058  rexss  4059  rabss2  4078  ssconb  4142  ssequn1  4186  unss  4190  ssin  4239  ssdif0  4366  difin0ss  4373  inssdif0  4374  reldisj  4453  ssundif  4488  sbcssg  4520  pwss  4623  snssb  4782  snssgOLD  4784  pwpw0  4813  ssuni  4932  unissb  4939  unissbOLD  4940  iunssf  5044  iunss  5045  dftr2  5261  axpweq  5351  axpow2  5367  ssextss  5458  ssrel  5792  ssrelOLD  5793  ssrel2  5795  ssrelrel  5806  reliun  5826  relop  5861  idrefALT  6131  funimass4  6973  dfom2  7889  inf2  9663  grothprim  10874  psslinpr  11071  ltaddpr  11074  isprm2  16719  vdwmc2  17017  acsmapd  18599  ismhp3  22146  dfconn2  23427  iskgen3  23557  metcld  25340  metcld2  25341  isch2  31242  pjnormssi  32187  ssiun3  32571  ssrelf  32627  bnj1361  34842  bnj978  34963  fineqvpow  35110  dffr5  35754  brsset  35890  sscoid  35914  ss-ax8  36226  relowlpssretop  37365  fvineqsneq  37413  unielss  43230  rp-fakeinunass  43528  rababg  43587  dfhe3  43788  snhesn  43799  dffrege76  43952  ntrneiiso  44104  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  expanduniss  44312  ismnuprim  44313  ismnushort  44320  onfrALTlem2  44566  trsspwALT  44838  trsspwALT2  44839  snssiALTVD  44847  snssiALT  44848  sstrALT2VD  44854  sstrALT2  44855  sbcssgVD  44903  onfrALTlem2VD  44909  sspwimp  44938  sspwimpVD  44939  sspwimpcf  44940  sspwimpcfVD  44941  sspwimpALT  44945  unisnALT  44946  ssclaxsep  44999  icccncfext  45902