Definition df-ss 3934

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

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 11083 and 1ex 11177) or ℝ ( cf. df-r 11085 and reex 11166). 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 11166). 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 3935. (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 3917	. 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  3935  dfss3  3938  dfss6  3939  dfssf  3940  ssel  3943  ssriv  3953  ssrdv  3955  sstr2  3956  sstr2OLD  3957  eqss  3965  nss  4014  ssralv  4018  ssrexv  4019  ralss  4024  rexss  4025  rabss2  4044  ssconb  4108  ssequn1  4152  unss  4156  ssin  4205  ssdif0  4332  difin0ss  4339  inssdif0  4340  reldisj  4419  ssundif  4454  sbcssg  4486  pwss  4589  snssb  4749  snssgOLD  4751  pwpw0  4780  ssuni  4899  unissb  4906  unissbOLD  4907  iunssf  5011  iunss  5012  dftr2  5219  axpweq  5309  axpow2  5325  ssextss  5416  ssrel  5748  ssrelOLD  5749  ssrel2  5751  ssrelrel  5762  reliun  5782  relop  5817  idrefALT  6087  funimass4  6928  dfom2  7847  inf2  9583  grothprim  10794  psslinpr  10991  ltaddpr  10994  isprm2  16659  vdwmc2  16957  acsmapd  18520  ismhp3  22036  dfconn2  23313  iskgen3  23443  metcld  25213  metcld2  25214  isch2  31159  pjnormssi  32104  ssiun3  32494  ssrelf  32550  bnj1361  34825  bnj978  34946  fineqvpow  35093  dffr5  35748  brsset  35884  sscoid  35908  ss-ax8  36220  relowlpssretop  37359  fvineqsneq  37407  unielss  43214  rp-fakeinunass  43511  rababg  43570  dfhe3  43771  snhesn  43782  dffrege76  43935  ntrneiiso  44087  ntrneik2  44088  ntrneix2  44089  ntrneikb  44090  expanduniss  44289  ismnuprim  44290  ismnushort  44297  onfrALTlem2  44543  trsspwALT  44814  trsspwALT2  44815  snssiALTVD  44823  snssiALT  44824  sstrALT2VD  44830  sstrALT2  44831  sbcssgVD  44879  onfrALTlem2VD  44885  sspwimp  44914  sspwimpVD  44915  sspwimpcf  44916  sspwimpcfVD  44917  sspwimpALT  44921  unisnALT  44922  ssclaxsep  44979  permaxpow  45006  icccncfext  45892