Metamath Proof Explorer

Table of Contents - 21.27.23. Type-safe Partition-Equivalence: PetParts, PetErs, Pet2Parts, Pet2Ers

1. df-petparts
2. df-peters
3. df-pet2parts
4. df-pet2ers
5. dfpetparts2
6. dfpet2parts2
7. dfpeters2
8. typesafepets
9. petseq
10. pets2eq