Definition df-ss 3993

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30459). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4031). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3996). For an alternative definition, not requiring a dummy variable, see dfss2 3994. Other possible definitions are given by dfss3 3997, dfss4 4288, sspss 4125, ssequn1 4209, ssequn2 4212, sseqin2 4244, and ssdif0 4389.

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 11192 and 1ex 11286) or ℝ ( cf. df-r 11194 and reex 11275). 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 11275). 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 3994. (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 3976	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1536	. . . . 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 1535	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 206	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3994  dfss3  3997  dfss6  3998  dfssf  3999  ssel  4002  ssriv  4012  ssrdv  4014  sstr2  4015  sstr2OLD  4016  eqss  4024  nss  4073  ssralv  4077  ssrexv  4078  rabss2  4101  ssconb  4165  ssequn1  4209  unss  4213  ssin  4260  ssdif0  4389  difin0ss  4396  inssdif0  4397  reldisj  4476  ssundif  4511  sbcssg  4543  pwss  4645  snssb  4807  snssgOLD  4809  pwpw0  4838  ssuni  4956  unissb  4963  unissbOLD  4964  iunssf  5067  iunss  5068  dftr2  5285  axpweq  5369  axpow2  5385  ssextss  5473  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  reliun  5840  relop  5875  idrefALT  6143  funimass4  6986  dfom2  7905  inf2  9692  grothprim  10903  psslinpr  11100  ltaddpr  11103  isprm2  16729  vdwmc2  17026  acsmapd  18624  ismhp3  22169  dfconn2  23448  iskgen3  23578  metcld  25359  metcld2  25360  isch2  31255  pjnormssi  32200  ssiun3  32581  ssrelf  32637  bnj1361  34804  bnj978  34925  fineqvpow  35072  dffr5  35716  brsset  35853  sscoid  35877  ss-ax8  36191  relowlpssretop  37330  fvineqsneq  37378  unielss  43179  rp-fakeinunass  43477  rababg  43536  dfhe3  43737  snhesn  43748  dffrege76  43901  ntrneiiso  44053  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  expanduniss  44262  ismnuprim  44263  ismnushort  44270  onfrALTlem2  44517  trsspwALT  44789  trsspwALT2  44790  snssiALTVD  44798  snssiALT  44799  sstrALT2VD  44805  sstrALT2  44806  sbcssgVD  44854  onfrALTlem2VD  44860  sspwimp  44889  sspwimpVD  44890  sspwimpcf  44891  sspwimpcfVD  44892  sspwimpALT  44896  unisnALT  44897  icccncfext  45808