Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-pss | Unicode version | ||
Description: Define proper subclass
relationship between two classes. Definition 5.9
of [TakeutiZaring] p. 17. For
example,  1 , 2
  1 , 2 , 3
(ex-pss in
set.mm). Note that   (proved in pssirr 3369).
Contrast this relationship with the relationship   (as defined in
df-ss 3259). Other possible definitions are given by dfpss2 3354 and
dfpss3 3355. (Contributed by NM,
7-Feb-1996.) |
| Ref | Expression |
|---|---|
| df-pss |
   ![](wedge.gif "/\"){kind=small}   |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | cB |
. . 3
| |
| 3 | 1, 2 | wpss 3258 |
. 2
 |
| 4 | 1, 2 | wss 3257 |
. . 3
|
| 5 | 1, 2 | wne 2516 |
. . 3
|
| 6 | 4, 5 | wa 358 |
. 2
|
| 7 | 3, 6 | wb 176 |
1
|
| Colors of variables: wff setvar class |
| This definition is referenced by: dfpss2 3354 psseq1 3356 psseq2 3357 pssss 3364 pssne 3365 nssinpss 3487 0pss 3588 pssdif 3612 difsnpss 3851 sfinltfin 4535 |
| Copyright terms: Public domain | W3C validator |