Metamath Proof Explorer
Table of Contents - 7.1.1.1. Extensible structures as structures with components
- cstr
- df-struct
- brstruct
- isstruct2
- structex
- structn0fun
- isstruct
- structcnvcnv
- structfung
- structfun
- structfn
- strleun
- strle1
- strle2
- strle3
- sbcie2s
- sbcie3s