Metamath Proof Explorer

Table of Contents - 21.5. Mathbox for BTernaryTau

1. First-order logic
   1. Auxiliary axiom schemes
2. ZF set theory
   1. inv2
   2. jaeqifi
   3. exdifsn
   4. axnulALT2
   5. f1preimaex
   6. fnfvintima
   7. ordprcon
   8. xoromon
   9. soinfdom
   10. abweex
   11. ordtypeon
   12. fnrelpredd
   13. cardpred
   14. nummin
   15. 1enumen
   16. 1enumcard
   17. r11
   18. r12
   19. onrankid
   20. rankfilimb
   21. r1filim
   22. r1omfi
   23. r1omhf
   24. r1ssel
   25. axnulALT3
   26. axprALT2
   27. rankfo
   28. rankfn
   29. trssfir1om
   30. r1omhfb
   31. werankwe
   32. scotteqi
   33. elscott
   34. dfscott2
   35. dfscott3
   36. elscott2
   37. elscottrank
   38. elscottrankeq
   39. elscottrankss
   40. scottrankeqel
   41. nelscottrankgt
   42. scottsn
   43. scott0bOLD
   44. rankscott
   45. rankscottu
   46. scottssr1
   47. acnum
   48. weexenwe
   49. infinfnum
   50. rncardr1prc
   51. acwer1prclem
   52. acwer1prc
   53. Ordinals 5 through 9
   54. Finitism
   55. Introduce ax-regs
   56. Derive ax-regs
   57. ZFC axioms with reduced distinct variable conditions
   58. Cardinality without the Axiom of Choice
   59. Gödel operations
   60. The constructible universe
   61. Global choice
3. Real and complex numbers
   1. zltp1ne
   2. nnltp1ne
   3. nn0ltp1ne
   4. fisshasheq
   5. 1enum
4. Graph theory
   1. cplgredgex
   2. cusgredgex
   3. cusgredgex2
   4. revwlkb
   5. usgrgt2cycl
   6. usgrcyclgt2v
   7. cusgr3cyclex
   8. 2cycl2d
   9. Acyclic graphs