Metamath Proof Explorer
Table of Contents - 2.4.11. Function transposition
- ctpos
- df-tpos
- tposss
- tposeq
- tposeqd
- tposssxp
- reltpos
- brtpos2
- brtpos0
- reldmtpos
- brtpos
- ottpos
- relbrtpos
- dmtpos
- rntpos
- tposexg
- ovtpos
- tposfun
- dftpos2
- dftpos3
- dftpos4
- tpostpos
- tpostpos2
- tposfn2
- tposfo2
- tposf2
- tposf12
- tposf1o2
- tposfo
- tposf
- tposfn
- tpos0
- tposco
- tpossym
- tposeqi
- tposex
- nftpos
- tposoprab
- tposmpo
- tposconst