![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-ss | Structured version Visualization version GIF version |
Description: Define the subclass
relationship. Definition 5.9 of [TakeutiZaring]
p. 17. For example, {1, 2} ⊆ {1, 2, 3}
(ex-ss 30360). Note
that 𝐴 ⊆ 𝐴 (proved in ssid 4002). Contrast this relationship with
the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3967). For an
alternative definition, not requiring a dummy variable, see dfss2 3965.
Other possible definitions are given by dfss3 3968, dfss4 4260, sspss 4098,
ssequn1 4181, ssequn2 4184, sseqin2 4216, and ssdif0 4366.
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 11166 and 1ex 11260) or ℝ ( cf. df-r 11168 and reex 11249). 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 11249). 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 3965. (Revised by GG, 15-May-2025.) |
Ref | Expression |
---|---|
df-ss | ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wss 3947 | . 2 wff 𝐴 ⊆ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1533 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2099 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 5, 2 | wcel 2099 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) |
9 | 8, 4 | wal 1532 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 205 | 1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfss2 3965 dfss3 3968 dfss6 3969 dfssf 3970 ssel 3973 ssriv 3983 ssrdv 3985 sstr2 3986 sstr2OLD 3987 eqss 3995 nss 4044 ssralv 4048 ssrexv 4049 rabss2 4074 ssconb 4137 ssequn1 4181 unss 4185 ssin 4232 ssdif0 4366 difin0ss 4373 inssdif0 4374 reldisj 4456 reldisjOLD 4457 ssundif 4492 sbcssg 4528 pwss 4630 snssb 4791 snssgOLD 4793 pwpw0 4822 ssuni 4940 unissb 4947 unissbOLD 4948 iunssf 5052 iunss 5053 dftr2 5272 axpweq 5354 axpow2 5371 ssextss 5459 ssrel 5788 ssrelOLD 5789 ssrel2 5791 ssrelrel 5802 reliun 5822 relop 5857 idrefALT 6123 funimass4 6967 dfom2 7878 inf2 9666 grothprim 10877 psslinpr 11074 ltaddpr 11077 isprm2 16683 vdwmc2 16981 acsmapd 18579 ismhp3 22137 dfconn2 23414 iskgen3 23544 metcld 25325 metcld2 25326 isch2 31156 pjnormssi 32101 ssiun3 32479 ssrelf 32535 bnj1361 34673 bnj978 34794 fineqvpow 34932 dffr5 35576 brsset 35713 sscoid 35737 relowlpssretop 37071 fvineqsneq 37119 unielss 42883 rp-fakeinunass 43182 rababg 43241 dfhe3 43442 snhesn 43453 dffrege76 43606 ntrneiiso 43758 ntrneik2 43759 ntrneix2 43760 ntrneikb 43761 expanduniss 43967 ismnuprim 43968 ismnushort 43975 onfrALTlem2 44222 trsspwALT 44494 trsspwALT2 44495 snssiALTVD 44503 snssiALT 44504 sstrALT2VD 44510 sstrALT2 44511 sbcssgVD 44559 onfrALTlem2VD 44565 sspwimp 44594 sspwimpVD 44595 sspwimpcf 44596 sspwimpcfVD 44597 sspwimpALT 44601 unisnALT 44602 icccncfext 45508 |
Copyright terms: Public domain | W3C validator |