Definition df-ss 3907

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30517). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3945). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3910). For an alternative definition, not requiring a dummy variable, see dfss2 3908. Other possible definitions are given by dfss3 3911, dfss4 4210, sspss 4043, ssequn1 4127, ssequn2 4130, sseqin2 4164, and ssdif0 4307.

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 11035 and 1ex 11129) or ℝ ( cf. df-r 11037 and reex 11118). 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 11118). 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 3908. (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 3890	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1541	. . . . 5 class 𝑥
6	5, 1	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
9	8, 4	wal 1540	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 206	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3908  dfss3  3911  dfss6  3912  dfssf  3913  ssel  3916  ssriv  3926  ssrdv  3928  sstr2  3929  sstr2OLD  3930  eqss  3938  nss  3987  ssralv  3991  ssrexv  3992  ralss  3997  rexss  3998  rabss2OLD  4019  ssconb  4083  ssequn1  4127  unss  4131  ssin  4180  ssdif0  4307  difin0ss  4314  inssdif0  4315  reldisj  4394  ssundif  4428  sbcssg  4462  pwss  4565  snssb  4727  pwpw0  4757  ssuni  4876  unissb  4884  iunssf  4986  iunssfOLD  4987  iunss  4988  iunssOLD  4989  dftr2  5195  axpweq  5286  axpow2  5302  ssextss  5398  ssrel  5730  ssrel2  5732  ssrelrel  5743  relop  5797  idrefALT  6068  funimass4  6896  dfom2  7810  inf2  9533  grothprim  10746  psslinpr  10943  ltaddpr  10946  isprm2  16640  vdwmc2  16939  acsmapd  18509  ismhp3  22117  dfconn2  23393  iskgen3  23523  metcld  25282  metcld2  25283  isch2  31314  pjnormssi  32259  ssiun3  32648  ssrelf  32708  bnj1361  34991  bnj978  35112  r1omhfb  35277  fineqvpow  35280  r1omhfbregs  35302  dffr5  35957  brsset  36090  sscoid  36114  ss-ax8  36428  axtco  36674  axtco1g  36679  regsfromregtco  36741  relowlpssretop  37691  fvineqsneq  37739  unielss  43661  rp-fakeinunass  43957  rababg  44016  dfhe3  44217  snhesn  44228  dffrege76  44381  ntrneiiso  44533  ntrneik2  44534  ntrneix2  44535  ntrneikb  44536  expanduniss  44735  ismnuprim  44736  ismnushort  44743  onfrALTlem2  44988  trsspwALT  45259  trsspwALT2  45260  snssiALTVD  45268  snssiALT  45269  sstrALT2VD  45275  sstrALT2  45276  sbcssgVD  45324  onfrALTlem2VD  45330  sspwimp  45359  sspwimpVD  45360  sspwimpcf  45361  sspwimpcfVD  45362  sspwimpALT  45366  unisnALT  45367  ssclaxsep  45424  permaxpow  45451  icccncfext  46330