| 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 30447). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4103). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3968). Other possible definitions are given by dfpss2 4088 and dfpss3 4089. (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 3952 | . 2 wff 𝐴 ⊊ 𝐵 |
| 4 | 1, 2 | wss 3951 | . . 3 wff 𝐴 ⊆ 𝐵 |
| 5 | 1, 2 | wne 2940 | . . 3 wff 𝐴 ≠ 𝐵 |
| 6 | 4, 5 | wa 395 | . 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) |
| 7 | 3, 6 | wb 206 | 1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfpss2 4088 psseq1 4090 psseq2 4091 pssss 4098 pssne 4099 nssinpss 4267 pssdif 4369 0pss 4447 difsnpss 4807 ordelpss 6412 fisseneq 9293 ominf 9294 ominfOLD 9295 f1finf1o 9305 f1finf1oOLD 9306 fofinf1o 9372 inf3lem2 9669 inf3lem4 9671 infeq5 9677 fin23lem31 10383 isf32lem6 10398 ipolt 18580 lssnle 19692 pgpfaclem2 20102 lspsncv0 21148 islbs3 21157 lbsextlem4 21163 lidlnz 21252 filssufilg 23919 alexsubALTlem4 24058 ppiltx 27220 ex-pss 30447 ch0pss 31464 exsslsb 33647 nepss 35718 dfon2 35793 relowlpssretop 37365 finxpreclem3 37394 fin2solem 37613 lshpnelb 38985 lshpcmp 38989 lsatssn0 39003 lcvbr3 39024 lsatcv0 39032 lsat0cv 39034 lcvexchlem1 39035 islshpcv 39054 lkrpssN 39164 lkreqN 39171 osumcllem11N 39968 pexmidlem8N 39979 dochsordN 41376 dochsat 41385 dochshpncl 41386 dochexmidlem8 41469 mapdsord 41657 psspwb 42267 xppss12 42268 omssrncard 43553 trelpss 44474 isomenndlem 46545 lvecpsslmod 48424 |
| Copyright terms: Public domain | W3C validator |