![]() |
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 3019). For a more traditional definition, but requiring a dummy variable, see dfss2 2989. Other possible definitions are given by dfss3 2990, ssequn1 3143, ssequn2 3146, and sseqin2 3192. (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 2974 | . 2 wff 𝐴 ⊆ 𝐵 |
4 | 1, 2 | cin 2973 | . . 3 class (𝐴 ∩ 𝐵) |
5 | 4, 1 | wceq 1285 | . 2 wff (𝐴 ∩ 𝐵) = 𝐴 |
6 | 3, 5 | wb 103 | 1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: dfss 2988 dfss1 3177 inabs 3204 dfrab3ss 3249 disjssun 3314 riinm 3758 rintm 3773 ssex 3923 op1stb 4235 op1stbg 4236 ssdmres 4661 resima2 4672 xpssres 4673 fnimaeq0 5051 fnreseql 5309 tpostpos2 5914 tfrexlem 5983 ecinxp 6247 uzin 8732 iooval2 9014 minmax 10250 2prm 10653 bdssex 10851 |
Copyright terms: Public domain | W3C validator |