Definition df-ss 3919

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30915). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3956). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3922). For an alternative definition, not requiring a dummy variable, see dfss2 3920. Other possible definitions are given by dfss3 3923, dfss4 4218, sspss 4053, ssequn1 4135, ssequn2 4138, sseqin2 4172, 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 11136 and 1ex 11231) or ℝ ( cf. df-r 11138 and reex 11219). 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 11219). 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 3920. (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 3902	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1569	. . . . 5 class 𝑥
6	5, 1	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
9	8, 4	wal 1568	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 209	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is used by:  dfss2  3920  dfss3  3923  dfss6  3924  dfssf  3925  ssel  3928  ssriv  3938  ssrdv  3940  sstr2  3941  eqss  3949  nss  3998  ssralv  4003  ssrexv  4004  ralss  4007  rexss  4008  rabss2OLD  4029  ssconb  4092  ssequn1  4135  unss  4139  ssin  4187  ssdif0  4317  difin0ss  4324  inssdif0OLD  4326  reldisj  4409  ssundif  4446  sbcssg  4480  pwss  4584  snssb  4746  pwpw0  4777  ssuni  4896  unissb  4904  iunssf  5005  iunssfOLD  5006  iunss  5007  iunssOLD  5008  dftr2  5218  axpweq  5319  axpow2  5336  ssextss  5432  ssrel  5767  ssrel2  5769  ssrelrel  5780  relop  5834  idrefALT  6111  funimass4  6946  dfom2  7868  inf2  9606  grothprim  10847  psslinpr  11044  ltaddpr  11047  isprm2  16778  vdwmc2  17077  acsmapd  18648  ismhp3  22376  dfconn2  23650  iskgen3  23781  metcld  25540  metcld2  25541  isch2  31712  pjnormssi  32657  ssiun3  33040  ssrelf  33096  bnj1361  35345  bnj978  35466  r1omhfb  35630  fineqvpow  35649  r1omhfbregs  35671  brsset  36474  sscoid  36498  ss-ax8  36853  axtco  37098  axtco1g  37103  regsfromregtco  37165  mh-infprim1bi  37173  mh-infprim2bi  37174  relowlpssretop  38126  fvineqsneq  38174  unielss  44067  rp-fakeinunass  44363  rababg  44422  dfhe3  44623  snhesn  44634  dffrege76  44787  ntrneiiso  44939  ntrneik2  44940  ntrneix2  44941  ntrneikb  44942  expanduniss  45125  ismnuprim  45126  ismnushort  45133  onfrALTlem2  45377  trsspwALT  45648  trsspwALT2  45649  snssiALTVD  45657  snssiALT  45658  sstrALT2VD  45664  sstrALT2  45665  sbcssgVD  45713  onfrALTlem2VD  45719  sspwimp  45748  sspwimpVD  45749  sspwimpcf  45750  sspwimpcfVD  45751  sspwimpALT  45755  unisnALT  45756  ssclaxsep  45813  permaxpow  45840  icccncfext  46723