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 30485). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3957). 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 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 11038 and 1ex 11132) or ℝ ( cf. df-r 11040 and reex 11121). 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 11121). 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 1541	. . . . 5 class 𝑥
6	5, 1	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
9	8, 4	wal 1540	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
10	3, 9	wb 206	1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

This definition is referenced by:  dfss2  3920  dfss3  3923  dfss6  3924  dfssf  3925  ssel  3928  ssriv  3938  ssrdv  3940  sstr2  3941  sstr2OLD  3942  eqss  3950  nss  3999  ssralv  4003  ssrexv  4004  ralss  4009  rexss  4010  rabss2OLD  4031  ssconb  4095  ssequn1  4139  unss  4143  ssin  4192  ssdif0  4319  difin0ss  4326  inssdif0  4327  reldisj  4406  ssundif  4441  sbcssg  4475  pwss  4578  snssb  4740  pwpw0  4770  ssuni  4889  unissb  4897  iunssf  4999  iunssfOLD  5000  iunss  5001  iunssOLD  5002  dftr2  5208  axpweq  5297  axpow2  5313  ssextss  5402  ssrel  5733  ssrel2  5735  ssrelrel  5746  relop  5800  idrefALT  6071  funimass4  6899  dfom2  7812  inf2  9536  grothprim  10749  psslinpr  10946  ltaddpr  10949  isprm2  16613  vdwmc2  16911  acsmapd  18481  ismhp3  22089  dfconn2  23367  iskgen3  23497  metcld  25266  metcld2  25267  isch2  31281  pjnormssi  32226  ssiun3  32615  ssrelf  32675  bnj1361  34965  bnj978  35086  r1omhfb  35249  fineqvpow  35252  r1omhfbregs  35274  dffr5  35929  brsset  36062  sscoid  36086  ss-ax8  36400  exeltr  36646  regsfromregtr  36649  relowlpssretop  37546  fvineqsneq  37594  unielss  43502  rp-fakeinunass  43798  rababg  43857  dfhe3  44058  snhesn  44069  dffrege76  44222  ntrneiiso  44374  ntrneik2  44375  ntrneix2  44376  ntrneikb  44377  expanduniss  44576  ismnuprim  44577  ismnushort  44584  onfrALTlem2  44829  trsspwALT  45100  trsspwALT2  45101  snssiALTVD  45109  snssiALT  45110  sstrALT2VD  45116  sstrALT2  45117  sbcssgVD  45165  onfrALTlem2VD  45171  sspwimp  45200  sspwimpVD  45201  sspwimpcf  45202  sspwimpcfVD  45203  sspwimpALT  45207  unisnALT  45208  ssclaxsep  45265  permaxpow  45292  icccncfext  46173