Metamath Proof Explorer

Table of Contents - 21.38.4.30. RP ADDTO: Finite induction (for finite ordinals)

Original probably needs new subsection for Relation-related existence theorems.

1. cnvcnvintabd