Metamath Proof Explorer

Table of Contents - 5.6.11.141. Finite induction on the size of the first component of a binary relation

1. hashdifsnp1
2. fi1uzind
3. brfi1uzind
4. brfi1ind
5. brfi1indALT
6. opfi1uzind
7. opfi1ind