Definition df-ss 3924

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30687). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3961). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3927). For an alternative definition, not requiring a dummy variable, see dfss2 3925. Other possible definitions are given by dfss3 3928, dfss4 4224, sspss 4058, ssequn1 4141, ssequn2 4144, sseqin2 4178, and ssdif0 4322.

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 11096 and 1ex 11191) or ℝ ( cf. df-r 11098 and reex 11179). 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 11179). 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 3925. (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 3907	. 2 wff 𝐴 ⊆ 𝐵
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1562	. . . . 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 1561	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 209	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3925  dfss3  3928  dfss6  3929  dfssf  3930  ssel  3933  ssriv  3943  ssrdv  3945  sstr2  3946  eqss  3954  nss  4003  ssralv  4008  ssrexv  4009  ralss  4012  rexss  4013  rabss2OLD  4034  ssconb  4098  ssequn1  4141  unss  4145  ssin  4193  ssdif0  4322  difin0ss  4329  inssdif0  4330  reldisj  4410  ssundif  4444  sbcssg  4478  pwss  4582  snssb  4744  pwpw0  4774  ssuni  4894  unissb  4902  iunssf  5003  iunssfOLD  5004  iunss  5005  iunssOLD  5006  dftr2  5214  axpweq  5312  axpow2  5329  ssextss  5425  ssrel  5760  ssrel2  5762  ssrelrel  5773  relop  5827  idrefALT  6104  funimass4  6935  dfom2  7852  inf2  9580  grothprim  10807  psslinpr  11004  ltaddpr  11007  isprm2  16730  vdwmc2  17029  acsmapd  18600  ismhp3  22265  dfconn2  23537  iskgen3  23667  metcld  25426  metcld2  25427  isch2  31484  pjnormssi  32429  ssiun3  32813  ssrelf  32872  bnj1361  35133  bnj978  35254  r1omhfb  35420  fineqvpow  35423  r1omhfbregs  35445  dffr5  36117  brsset  36250  sscoid  36274  ss-ax8  36598  axtco  36844  axtco1g  36849  regsfromregtco  36911  mh-infprim1bi  36919  mh-infprim2bi  36920  relowlpssretop  37870  fvineqsneq  37918  unielss  43807  rp-fakeinunass  44103  rababg  44162  dfhe3  44363  snhesn  44374  dffrege76  44527  ntrneiiso  44679  ntrneik2  44680  ntrneix2  44681  ntrneikb  44682  expanduniss  44867  ismnuprim  44868  ismnushort  44875  onfrALTlem2  45120  trsspwALT  45391  trsspwALT2  45392  snssiALTVD  45400  snssiALT  45401  sstrALT2VD  45407  sstrALT2  45408  sbcssgVD  45456  onfrALTlem2VD  45462  sspwimp  45491  sspwimpVD  45492  sspwimpcf  45493  sspwimpcfVD  45494  sspwimpALT  45498  unisnALT  45499  ssclaxsep  45556  permaxpow  45583  icccncfext  46459