Metamath Proof Explorer

Table of Contents - 2.3.11. The Predecessor Class

  1. cpred
  2. df-pred
  3. predeq123
  4. predeq1
  5. predeq2
  6. predeq3
  7. nfpred
  8. csbpredg
  9. predpredss
  10. predss
  11. sspred
  12. dfpred2
  13. dfpred3
  14. dfpred3g
  15. elpredgg
  16. elpredg
  17. elpredimg
  18. elpredim
  19. elpred
  20. predexg
  21. dffr4
  22. predel
  23. predtrss
  24. predpo
  25. predso
  26. setlikespec
  27. predidm
  28. predin
  29. predun
  30. preddif
  31. predep
  32. trpred
  33. preddowncl
  34. predpoirr
  35. predfrirr
  36. pred0
  37. dfse3
  38. predrelss
  39. predprc
  40. predres