Definition df-ss 3916

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30418). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3954). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3919). For an alternative definition, not requiring a dummy variable, see dfss2 3917. Other possible definitions are given by dfss3 3920, dfss4 4220, sspss 4053, ssequn1 4137, ssequn2 4140, sseqin2 4174, and ssdif0 4317.

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 11024 and 1ex 11118) or ℝ ( cf. df-r 11026 and reex 11107). 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 11107). 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 3917. (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 3899	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1540	. . . . 5 class 𝑥
6	5, 1	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
9	8, 4	wal 1539	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 206	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3917  dfss3  3920  dfss6  3921  dfssf  3922  ssel  3925  ssriv  3935  ssrdv  3937  sstr2  3938  sstr2OLD  3939  eqss  3947  nss  3996  ssralv  4000  ssrexv  4001  ralss  4006  rexss  4007  ss2abim  4010  rabss2OLD  4029  ssconb  4093  ssequn1  4137  unss  4141  ssin  4190  ssdif0  4317  difin0ss  4324  inssdif0  4325  reldisj  4404  ssundif  4439  sbcssg  4471  pwss  4574  snssb  4736  pwpw0  4766  ssuni  4885  unissb  4893  iunssf  4995  iunssfOLD  4996  iunss  4997  iunssOLD  4998  dftr2  5204  axpweq  5293  axpow2  5309  ssextss  5398  ssrel  5729  ssrel2  5731  ssrelrel  5742  reliunOLD  5763  relop  5797  idrefALT  6067  funimass4  6895  dfom2  7807  inf2  9523  grothprim  10735  psslinpr  10932  ltaddpr  10935  isprm2  16603  vdwmc2  16901  acsmapd  18470  ismhp3  22067  dfconn2  23344  iskgen3  23474  metcld  25243  metcld2  25244  isch2  31214  pjnormssi  32159  ssiun3  32549  ssrelf  32609  bnj1361  34851  bnj978  34972  r1omhfb  35134  r1omhfbregs  35144  fineqvpow  35149  dffr5  35809  brsset  35942  sscoid  35966  ss-ax8  36280  relowlpssretop  37419  fvineqsneq  37467  unielss  43325  rp-fakeinunass  43622  rababg  43681  dfhe3  43882  snhesn  43893  dffrege76  44046  ntrneiiso  44198  ntrneik2  44199  ntrneix2  44200  ntrneikb  44201  expanduniss  44400  ismnuprim  44401  ismnushort  44408  onfrALTlem2  44653  trsspwALT  44924  trsspwALT2  44925  snssiALTVD  44933  snssiALT  44934  sstrALT2VD  44940  sstrALT2  44941  sbcssgVD  44989  onfrALTlem2VD  44995  sspwimp  45024  sspwimpVD  45025  sspwimpcf  45026  sspwimpcfVD  45027  sspwimpALT  45031  unisnALT  45032  ssclaxsep  45089  permaxpow  45116  icccncfext  45999