Metamath Proof Explorer

Table of Contents - 2.4.14. Well-founded recursion

  1. cfrecs
  2. df-frecs
  3. frecseq123
  4. nffrecs
  5. csbfrecsg
  6. fpr3g
  7. frrlem1
  8. frrlem2
  9. frrlem3
  10. frrlem4
  11. frrlem5
  12. frrlem6
  13. frrlem7
  14. frrlem8
  15. frrlem9
  16. frrlem10
  17. frrlem11
  18. frrlem12
  19. frrlem13
  20. frrlem14
  21. fprlem1
  22. fprlem2
  23. fpr2a
  24. fpr1
  25. fpr2
  26. fpr3
  27. frrrel
  28. frrdmss
  29. frrdmcl
  30. fprfung
  31. fprresex