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. predpredss
  9. predss
  10. sspred
  11. dfpred2
  12. dfpred3
  13. dfpred3g
  14. elpredgg
  15. elpredg
  16. elpredimg
  17. elpredim
  18. elpred
  19. predasetex
  20. dffr4
  21. predel
  22. predpo
  23. predso
  24. predbrg
  25. setlikespec
  26. predidm
  27. predin
  28. predun
  29. preddif
  30. predep
  31. trpred
  32. preddowncl
  33. predpoirr
  34. predfrirr
  35. pred0