![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ss | GIF version |
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3177). For a more traditional definition, but requiring a dummy variable, see dfss2 3146. Other possible definitions are given by dfss3 3147, ssequn1 3307, ssequn2 3310, and sseqin2 3356. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
df-ss | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wss 3131 | . 2 wff 𝐴 ⊆ 𝐵 |
4 | 1, 2 | cin 3130 | . . 3 class (𝐴 ∩ 𝐵) |
5 | 4, 1 | wceq 1353 | . 2 wff (𝐴 ∩ 𝐵) = 𝐴 |
6 | 3, 5 | wb 105 | 1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: dfss 3145 dfss1 3341 inabs 3369 dfrab3ss 3415 disjssun 3488 riinm 3961 rintm 3981 ssex 4142 op1stb 4480 op1stbg 4481 ssdmres 4931 resima2 4943 xpssres 4944 fnimaeq0 5339 f0rn0 5412 fnreseql 5629 tpostpos2 6269 tfrexlem 6338 ecinxp 6613 uzin 9563 iooval2 9918 minmax 11241 xrminmax 11276 2prm 12130 dfphi2 12223 ressbas2d 12531 ressval3d 12534 restid2 12703 lidlbas 13601 difopn 13796 restopnb 13869 cnrest2 13924 bdssex 14842 |
Copyright terms: Public domain | W3C validator |