Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-pss | GIF version |
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 3044). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 2931). Other possible definitions are given by dfpss2 3029 and dfpss3 3030. (Contributed by NM, 7-Feb-1996.) |
Ref | Expression |
---|---|
df-pss | ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wpss 2918 | . 2 wff 𝐴 ⊊ 𝐵 |
4 | 1, 2 | wss 2917 | . . 3 wff 𝐴 ⊆ 𝐵 |
5 | 1, 2 | wne 2204 | . . 3 wff 𝐴 ≠ 𝐵 |
6 | 4, 5 | wa 97 | . 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) |
7 | 3, 6 | wb 98 | 1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: dfpss2 3029 psseq1 3031 psseq2 3032 pssss 3039 pssne 3040 nssinpss 3169 0pss 3265 difsnpssim 3507 |
Copyright terms: Public domain | W3C validator |