Metamath Proof Explorer
Table of Contents - 8.1.2. Opposite category
- coppc
- df-oppc
- oppcval
- oppchomfval
- oppchomfvalOLD
- oppchom
- oppccofval
- oppcco
- oppcbas
- oppcbasOLD
- oppccatid
- oppchomf
- oppcid
- oppccat
- 2oppcbas
- 2oppchomf
- 2oppccomf
- oppchomfpropd
- oppccomfpropd
- oppccatf