Metamath Proof Explorer

Table of Contents - 20.3.9.18. Scalar restriction operation

  1. cresv
  2. df-resv
  3. reldmresv
  4. resvval
  5. resvid2
  6. resvval2
  7. resvsca
  8. resvlem
  9. resvlemOLD
  10. resvbas
  11. resvbasOLD
  12. resvplusg
  13. resvplusgOLD
  14. resvvsca
  15. resvvscaOLD
  16. resvmulr
  17. resvmulrOLD
  18. resv0g
  19. resv1r
  20. resvcmn