Definition df-ss 3922

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30389). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3960). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3925). For an alternative definition, not requiring a dummy variable, see dfss2 3923. Other possible definitions are given by dfss3 3926, dfss4 4222, sspss 4055, ssequn1 4139, ssequn2 4142, sseqin2 4176, and ssdif0 4319.

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 11036 and 1ex 11130) or ℝ ( cf. df-r 11038 and reex 11119). 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 11119). 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 3923. (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 3905	. 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  3923  dfss3  3926  dfss6  3927  dfssf  3928  ssel  3931  ssriv  3941  ssrdv  3943  sstr2  3944  sstr2OLD  3945  eqss  3953  nss  4002  ssralv  4006  ssrexv  4007  ralss  4012  rexss  4013  rabss2  4031  ssconb  4095  ssequn1  4139  unss  4143  ssin  4192  ssdif0  4319  difin0ss  4326  inssdif0  4327  reldisj  4406  ssundif  4441  sbcssg  4473  pwss  4576  snssb  4736  snssgOLD  4738  pwpw0  4767  ssuni  4886  unissb  4893  iunssf  4996  iunss  4997  dftr2  5204  axpweq  5293  axpow2  5309  ssextss  5400  ssrel  5730  ssrel2  5732  ssrelrel  5743  reliun  5763  relop  5797  idrefALT  6066  funimass4  6891  dfom2  7808  inf2  9538  grothprim  10747  psslinpr  10944  ltaddpr  10947  isprm2  16611  vdwmc2  16909  acsmapd  18478  ismhp3  22045  dfconn2  23322  iskgen3  23452  metcld  25222  metcld2  25223  isch2  31185  pjnormssi  32130  ssiun3  32520  ssrelf  32576  bnj1361  34794  bnj978  34915  fineqvpow  35070  dffr5  35726  brsset  35862  sscoid  35886  ss-ax8  36198  relowlpssretop  37337  fvineqsneq  37385  unielss  43191  rp-fakeinunass  43488  rababg  43547  dfhe3  43748  snhesn  43759  dffrege76  43912  ntrneiiso  44064  ntrneik2  44065  ntrneix2  44066  ntrneikb  44067  expanduniss  44266  ismnuprim  44267  ismnushort  44274  onfrALTlem2  44520  trsspwALT  44791  trsspwALT2  44792  snssiALTVD  44800  snssiALT  44801  sstrALT2VD  44807  sstrALT2  44808  sbcssgVD  44856  onfrALTlem2VD  44862  sspwimp  44891  sspwimpVD  44892  sspwimpcf  44893  sspwimpcfVD  44894  sspwimpALT  44898  unisnALT  44899  ssclaxsep  44956  permaxpow  44983  icccncfext  45869