Definition df-ss 3914

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30414). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3952). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3917). For an alternative definition, not requiring a dummy variable, see dfss2 3915. Other possible definitions are given by dfss3 3918, dfss4 4218, sspss 4051, ssequn1 4135, ssequn2 4138, sseqin2 4172, and ssdif0 4315.

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 11020 and 1ex 11114) or ℝ ( cf. df-r 11022 and reex 11103). 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 11103). 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 3915. (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 3897	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1540	. . . . 5 class 𝑥
6	5, 1	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2111	. . . 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  3915  dfss3  3918  dfss6  3919  dfssf  3920  ssel  3923  ssriv  3933  ssrdv  3935  sstr2  3936  sstr2OLD  3937  eqss  3945  nss  3994  ssralv  3998  ssrexv  3999  ralss  4004  rexss  4005  ss2abim  4008  rabss2OLD  4027  ssconb  4091  ssequn1  4135  unss  4139  ssin  4188  ssdif0  4315  difin0ss  4322  inssdif0  4323  reldisj  4402  ssundif  4437  sbcssg  4469  pwss  4572  snssb  4734  pwpw0  4764  ssuni  4883  unissb  4891  iunssf  4993  iunssfOLD  4994  iunss  4995  iunssOLD  4996  dftr2  5202  axpweq  5291  axpow2  5307  ssextss  5396  ssrel  5727  ssrel2  5729  ssrelrel  5740  reliunOLD  5761  relop  5795  idrefALT  6065  funimass4  6892  dfom2  7804  inf2  9519  grothprim  10731  psslinpr  10928  ltaddpr  10931  isprm2  16599  vdwmc2  16897  acsmapd  18466  ismhp3  22063  dfconn2  23340  iskgen3  23470  metcld  25239  metcld2  25240  isch2  31210  pjnormssi  32155  ssiun3  32545  ssrelf  32605  bnj1361  34847  bnj978  34968  r1omhfb  35130  r1omhfbregs  35140  fineqvpow  35145  dffr5  35805  brsset  35938  sscoid  35962  ss-ax8  36276  relowlpssretop  37415  fvineqsneq  37463  unielss  43316  rp-fakeinunass  43613  rababg  43672  dfhe3  43873  snhesn  43884  dffrege76  44037  ntrneiiso  44189  ntrneik2  44190  ntrneix2  44191  ntrneikb  44192  expanduniss  44391  ismnuprim  44392  ismnushort  44399  onfrALTlem2  44644  trsspwALT  44915  trsspwALT2  44916  snssiALTVD  44924  snssiALT  44925  sstrALT2VD  44931  sstrALT2  44932  sbcssgVD  44980  onfrALTlem2VD  44986  sspwimp  45015  sspwimpVD  45016  sspwimpcf  45017  sspwimpcfVD  45018  sspwimpALT  45022  unisnALT  45023  ssclaxsep  45080  permaxpow  45107  icccncfext  45990