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. predasetexOLD
  22. dffr4
  23. predel
  24. predbrg
  25. predtrss
  26. predpo
  27. predso
  28. setlikespec
  29. predidm
  30. predin
  31. predun
  32. preddif
  33. predep
  34. trpred
  35. preddowncl
  36. predpoirr
  37. predfrirr
  38. pred0
  39. dfse3
  40. predrelss
  41. predprc
  42. predres