Definition df-ss 3917

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30397). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3955). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3920). For an alternative definition, not requiring a dummy variable, see dfss2 3918. Other possible definitions are given by dfss3 3921, dfss4 4217, sspss 4050, ssequn1 4134, ssequn2 4137, sseqin2 4171, and ssdif0 4314.

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 11006 and 1ex 11100) or ℝ ( cf. df-r 11008 and reex 11089). 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 11089). 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 3918. (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 3900	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1540	. . . . 5 class 𝑥
6	5, 1	wcel 2110	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2110	. . . 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  3918  dfss3  3921  dfss6  3922  dfssf  3923  ssel  3926  ssriv  3936  ssrdv  3938  sstr2  3939  sstr2OLD  3940  eqss  3948  nss  3997  ssralv  4001  ssrexv  4002  ralss  4007  rexss  4008  rabss2  4026  ssconb  4090  ssequn1  4134  unss  4138  ssin  4187  ssdif0  4314  difin0ss  4321  inssdif0  4322  reldisj  4401  ssundif  4436  sbcssg  4468  pwss  4571  snssb  4733  pwpw0  4763  ssuni  4882  unissb  4889  iunssf  4991  iunss  4992  dftr2  5198  axpweq  5287  axpow2  5303  ssextss  5392  ssrel  5721  ssrel2  5723  ssrelrel  5734  reliun  5754  relop  5788  idrefALT  6057  funimass4  6881  dfom2  7793  inf2  9508  grothprim  10717  psslinpr  10914  ltaddpr  10917  isprm2  16585  vdwmc2  16883  acsmapd  18452  ismhp3  22050  dfconn2  23327  iskgen3  23457  metcld  25226  metcld2  25227  isch2  31193  pjnormssi  32138  ssiun3  32528  ssrelf  32588  bnj1361  34830  bnj978  34951  fineqvpow  35106  dffr5  35766  brsset  35902  sscoid  35926  ss-ax8  36238  relowlpssretop  37377  fvineqsneq  37425  unielss  43230  rp-fakeinunass  43527  rababg  43586  dfhe3  43787  snhesn  43798  dffrege76  43951  ntrneiiso  44103  ntrneik2  44104  ntrneix2  44105  ntrneikb  44106  expanduniss  44305  ismnuprim  44306  ismnushort  44313  onfrALTlem2  44558  trsspwALT  44829  trsspwALT2  44830  snssiALTVD  44838  snssiALT  44839  sstrALT2VD  44845  sstrALT2  44846  sbcssgVD  44894  onfrALTlem2VD  44900  sspwimp  44929  sspwimpVD  44930  sspwimpcf  44931  sspwimpcfVD  44932  sspwimpALT  44936  unisnALT  44937  ssclaxsep  44994  permaxpow  45021  icccncfext  45904