Definition df-ss 3931

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30356). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3969). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3934). For an alternative definition, not requiring a dummy variable, see dfss2 3932. Other possible definitions are given by dfss3 3935, dfss4 4232, sspss 4065, ssequn1 4149, ssequn2 4152, sseqin2 4186, and ssdif0 4329.

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 11076 and 1ex 11170) or ℝ ( cf. df-r 11078 and reex 11159). 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 11159). 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 3932. (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 3914	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1539	. . . . 5 class 𝑥
6	5, 1	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2109	. . . 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  3932  dfss3  3935  dfss6  3936  dfssf  3937  ssel  3940  ssriv  3950  ssrdv  3952  sstr2  3953  sstr2OLD  3954  eqss  3962  nss  4011  ssralv  4015  ssrexv  4016  ralss  4021  rexss  4022  rabss2  4041  ssconb  4105  ssequn1  4149  unss  4153  ssin  4202  ssdif0  4329  difin0ss  4336  inssdif0  4337  reldisj  4416  ssundif  4451  sbcssg  4483  pwss  4586  snssb  4746  snssgOLD  4748  pwpw0  4777  ssuni  4896  unissb  4903  unissbOLD  4904  iunssf  5008  iunss  5009  dftr2  5216  axpweq  5306  axpow2  5322  ssextss  5413  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  reliun  5779  relop  5814  idrefALT  6084  funimass4  6925  dfom2  7844  inf2  9576  grothprim  10787  psslinpr  10984  ltaddpr  10987  isprm2  16652  vdwmc2  16950  acsmapd  18513  ismhp3  22029  dfconn2  23306  iskgen3  23436  metcld  25206  metcld2  25207  isch2  31152  pjnormssi  32097  ssiun3  32487  ssrelf  32543  bnj1361  34818  bnj978  34939  fineqvpow  35086  dffr5  35741  brsset  35877  sscoid  35901  ss-ax8  36213  relowlpssretop  37352  fvineqsneq  37400  unielss  43207  rp-fakeinunass  43504  rababg  43563  dfhe3  43764  snhesn  43775  dffrege76  43928  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  expanduniss  44282  ismnuprim  44283  ismnushort  44290  onfrALTlem2  44536  trsspwALT  44807  trsspwALT2  44808  snssiALTVD  44816  snssiALT  44817  sstrALT2VD  44823  sstrALT2  44824  sbcssgVD  44872  onfrALTlem2VD  44878  sspwimp  44907  sspwimpVD  44908  sspwimpcf  44909  sspwimpcfVD  44910  sspwimpALT  44914  unisnALT  44915  ssclaxsep  44972  permaxpow  44999  icccncfext  45885