Definition df-ss 3943

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30354). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3981). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3946). For an alternative definition, not requiring a dummy variable, see dfss2 3944. Other possible definitions are given by dfss3 3947, dfss4 4244, sspss 4077, ssequn1 4161, ssequn2 4164, sseqin2 4198, and ssdif0 4341.

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 11135 and 1ex 11229) or ℝ ( cf. df-r 11137 and reex 11218). 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 11218). 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 3944. (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 3926	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1539	. . . . 5 class 𝑥
6	5, 1	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2108	. . . 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  3944  dfss3  3947  dfss6  3948  dfssf  3949  ssel  3952  ssriv  3962  ssrdv  3964  sstr2  3965  sstr2OLD  3966  eqss  3974  nss  4023  ssralv  4027  ssrexv  4028  ralss  4033  rexss  4034  rabss2  4053  ssconb  4117  ssequn1  4161  unss  4165  ssin  4214  ssdif0  4341  difin0ss  4348  inssdif0  4349  reldisj  4428  ssundif  4463  sbcssg  4495  pwss  4598  snssb  4758  snssgOLD  4760  pwpw0  4789  ssuni  4908  unissb  4915  unissbOLD  4916  iunssf  5020  iunss  5021  dftr2  5231  axpweq  5321  axpow2  5337  ssextss  5428  ssrel  5761  ssrelOLD  5762  ssrel2  5764  ssrelrel  5775  reliun  5795  relop  5830  idrefALT  6100  funimass4  6942  dfom2  7861  inf2  9635  grothprim  10846  psslinpr  11043  ltaddpr  11046  isprm2  16699  vdwmc2  16997  acsmapd  18562  ismhp3  22078  dfconn2  23355  iskgen3  23485  metcld  25256  metcld2  25257  isch2  31150  pjnormssi  32095  ssiun3  32485  ssrelf  32541  bnj1361  34805  bnj978  34926  fineqvpow  35073  dffr5  35717  brsset  35853  sscoid  35877  ss-ax8  36189  relowlpssretop  37328  fvineqsneq  37376  unielss  43189  rp-fakeinunass  43486  rababg  43545  dfhe3  43746  snhesn  43757  dffrege76  43910  ntrneiiso  44062  ntrneik2  44063  ntrneix2  44064  ntrneikb  44065  expanduniss  44265  ismnuprim  44266  ismnushort  44273  onfrALTlem2  44519  trsspwALT  44790  trsspwALT2  44791  snssiALTVD  44799  snssiALT  44800  sstrALT2VD  44806  sstrALT2  44807  sbcssgVD  44855  onfrALTlem2VD  44861  sspwimp  44890  sspwimpVD  44891  sspwimpcf  44892  sspwimpcfVD  44893  sspwimpALT  44897  unisnALT  44898  ssclaxsep  44955  permaxpow  44982  icccncfext  45864