Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-pss | Structured version Visualization version GIF version |
Description: Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 28207). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4077). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3952). Other possible definitions are given by dfpss2 4062 and dfpss3 4063. (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 3937 | . 2 wff 𝐴 ⊊ 𝐵 |
4 | 1, 2 | wss 3936 | . . 3 wff 𝐴 ⊆ 𝐵 |
5 | 1, 2 | wne 3016 | . . 3 wff 𝐴 ≠ 𝐵 |
6 | 4, 5 | wa 398 | . 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) |
7 | 3, 6 | wb 208 | 1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfpss2 4062 psseq1 4064 psseq2 4065 pssss 4072 pssne 4073 nssinpss 4233 pssdif 4326 0pss 4396 difsnpss 4740 ordelpss 6219 fisseneq 8729 ominf 8730 f1finf1o 8745 fofinf1o 8799 inf3lem2 9092 inf3lem4 9094 infeq5 9100 fin23lem31 9765 isf32lem6 9780 ipolt 17769 lssnle 18800 pgpfaclem2 19204 lspsncv0 19918 islbs3 19927 lbsextlem4 19933 lidlnz 20001 filssufilg 22519 alexsubALTlem4 22658 ppiltx 25754 ex-pss 28207 ch0pss 29222 nepss 32948 dfon2 33037 relowlpssretop 34648 finxpreclem3 34677 fin2solem 34893 lshpnelb 36135 lshpcmp 36139 lsatssn0 36153 lcvbr3 36174 lsatcv0 36182 lsat0cv 36184 lcvexchlem1 36185 islshpcv 36204 lkrpssN 36314 lkreqN 36321 osumcllem11N 37117 pexmidlem8N 37128 dochsordN 38525 dochsat 38534 dochshpncl 38535 dochexmidlem8 38618 mapdsord 38806 psspwb 39134 xppss12 39135 trelpss 40807 isomenndlem 42832 lvecpsslmod 44582 |
Copyright terms: Public domain | W3C validator |