| 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 30446). Note
that 𝐴 ⊆ 𝐴 (proved in ssid 4006). Contrast this relationship with
the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3971). For an
alternative definition, not requiring a dummy variable, see dfss2 3969.
Other possible definitions are given by dfss3 3972, dfss4 4269, sspss 4102,
ssequn1 4186, ssequn2 4189, sseqin2 4223, 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 11163 and 1ex 11257) or ℝ ( cf. df-r 11165 and reex 11246). 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 11246). 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 3969. (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 3951 | . 2 wff 𝐴 ⊆ 𝐵 |
| 4 | vx | . . . . . 6 setvar 𝑥 | |
| 5 | 4 | cv 1539 | . . . . 5 class 𝑥 |
| 6 | 5, 1 | wcel 2108 | . . . 4 wff 𝑥 ∈ 𝐴 |
| 7 | 5, 2 | wcel 2108 | . . . 4 wff 𝑥 ∈ 𝐵 |
| 8 | 6, 7 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) |
| 9 | 8, 4 | wal 1538 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) |
| 10 | 3, 9 | wb 206 | 1 wff (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfss2 3969 dfss3 3972 dfss6 3973 dfssf 3974 ssel 3977 ssriv 3987 ssrdv 3989 sstr2 3990 sstr2OLD 3991 eqss 3999 nss 4048 ssralv 4052 ssrexv 4053 ralss 4058 rexss 4059 rabss2 4078 ssconb 4142 ssequn1 4186 unss 4190 ssin 4239 ssdif0 4366 difin0ss 4373 inssdif0 4374 reldisj 4453 ssundif 4488 sbcssg 4520 pwss 4623 snssb 4782 snssgOLD 4784 pwpw0 4813 ssuni 4932 unissb 4939 unissbOLD 4940 iunssf 5044 iunss 5045 dftr2 5261 axpweq 5351 axpow2 5367 ssextss 5458 ssrel 5792 ssrelOLD 5793 ssrel2 5795 ssrelrel 5806 reliun 5826 relop 5861 idrefALT 6131 funimass4 6973 dfom2 7889 inf2 9663 grothprim 10874 psslinpr 11071 ltaddpr 11074 isprm2 16719 vdwmc2 17017 acsmapd 18599 ismhp3 22146 dfconn2 23427 iskgen3 23557 metcld 25340 metcld2 25341 isch2 31242 pjnormssi 32187 ssiun3 32571 ssrelf 32627 bnj1361 34842 bnj978 34963 fineqvpow 35110 dffr5 35754 brsset 35890 sscoid 35914 ss-ax8 36226 relowlpssretop 37365 fvineqsneq 37413 unielss 43230 rp-fakeinunass 43528 rababg 43587 dfhe3 43788 snhesn 43799 dffrege76 43952 ntrneiiso 44104 ntrneik2 44105 ntrneix2 44106 ntrneikb 44107 expanduniss 44312 ismnuprim 44313 ismnushort 44320 onfrALTlem2 44566 trsspwALT 44838 trsspwALT2 44839 snssiALTVD 44847 snssiALT 44848 sstrALT2VD 44854 sstrALT2 44855 sbcssgVD 44903 onfrALTlem2VD 44909 sspwimp 44938 sspwimpVD 44939 sspwimpcf 44940 sspwimpcfVD 44941 sspwimpALT 44945 unisnALT 44946 ssclaxsep 44999 icccncfext 45902 |
| Copyright terms: Public domain | W3C validator |