Definition df-ss 3920

Description: Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30514). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3958). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3923). For an alternative definition, not requiring a dummy variable, see dfss2 3921. Other possible definitions are given by dfss3 3924, dfss4 4223, sspss 4056, ssequn1 4140, ssequn2 4143, sseqin2 4177, and ssdif0 4320.

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 11046 and 1ex 11140) or ℝ ( cf. df-r 11048 and reex 11129). 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 11129). 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 3921. (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 3903	. 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  3921  dfss3  3924  dfss6  3925  dfssf  3926  ssel  3929  ssriv  3939  ssrdv  3941  sstr2  3942  sstr2OLD  3943  eqss  3951  nss  4000  ssralv  4004  ssrexv  4005  ralss  4010  rexss  4011  rabss2OLD  4032  ssconb  4096  ssequn1  4140  unss  4144  ssin  4193  ssdif0  4320  difin0ss  4327  inssdif0  4328  reldisj  4407  ssundif  4442  sbcssg  4476  pwss  4579  snssb  4741  pwpw0  4771  ssuni  4890  unissb  4898  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  dftr2  5209  axpweq  5298  axpow2  5314  ssextss  5408  ssrel  5740  ssrel2  5742  ssrelrel  5753  relop  5807  idrefALT  6078  funimass4  6906  dfom2  7820  inf2  9544  grothprim  10757  psslinpr  10954  ltaddpr  10957  isprm2  16621  vdwmc2  16919  acsmapd  18489  ismhp3  22097  dfconn2  23375  iskgen3  23505  metcld  25274  metcld2  25275  isch2  31310  pjnormssi  32255  ssiun3  32644  ssrelf  32704  bnj1361  35003  bnj978  35124  r1omhfb  35287  fineqvpow  35290  r1omhfbregs  35312  dffr5  35967  brsset  36100  sscoid  36124  ss-ax8  36438  exeltr  36684  regsfromregtr  36687  relowlpssretop  37608  fvineqsneq  37656  unielss  43564  rp-fakeinunass  43860  rababg  43919  dfhe3  44120  snhesn  44131  dffrege76  44284  ntrneiiso  44436  ntrneik2  44437  ntrneix2  44438  ntrneikb  44439  expanduniss  44638  ismnuprim  44639  ismnushort  44646  onfrALTlem2  44891  trsspwALT  45162  trsspwALT2  45163  snssiALTVD  45171  snssiALT  45172  sstrALT2VD  45178  sstrALT2  45179  sbcssgVD  45227  onfrALTlem2VD  45233  sspwimp  45262  sspwimpVD  45263  sspwimpcf  45264  sspwimpcfVD  45265  sspwimpALT  45269  unisnALT  45270  ssclaxsep  45327  permaxpow  45354  icccncfext  46234