![]() |
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 3059). For a more traditional definition, but requiring a dummy variable, see dfss2 3028. Other possible definitions are given by dfss3 3029, ssequn1 3185, ssequn2 3188, and sseqin2 3234. (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 3013 | . 2 wff 𝐴 ⊆ 𝐵 |
4 | 1, 2 | cin 3012 | . . 3 class (𝐴 ∩ 𝐵) |
5 | 4, 1 | wceq 1296 | . 2 wff (𝐴 ∩ 𝐵) = 𝐴 |
6 | 3, 5 | wb 104 | 1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: dfss 3027 dfss1 3219 inabs 3247 dfrab3ss 3293 disjssun 3365 riinm 3824 rintm 3843 ssex 3997 op1stb 4328 op1stbg 4329 ssdmres 4767 resima2 4779 xpssres 4780 fnimaeq0 5169 f0rn0 5240 fnreseql 5448 tpostpos2 6068 tfrexlem 6137 ecinxp 6407 uzin 9150 iooval2 9481 minmax 10792 xrminmax 10824 2prm 11551 dfphi2 11638 restid2 11828 difopn 11975 restopnb 12048 cnrest2 12102 bdssex 12505 |
Copyright terms: Public domain | W3C validator |