Metamath Proof Explorer

Table of Contents - 21.5. Mathbox for BTernaryTau

1. ZF set theory
   1. exdifsn
   2. srcmpltd
   3. prsrcmpltd
   4. dff15
   5. f1resveqaeq
   6. f1resrcmplf1dlem
   7. f1resrcmplf1d
   8. funen1cnv
   9. fnrelpredd
   10. cardpred
   11. nummin
   12. Finitism
2. Real and complex numbers
   1. zltp1ne
   2. nnltp1ne
   3. nn0ltp1ne
   4. 0nn0m1nnn0
   5. f1resfz0f1d
   6. fisshasheq
   7. hashf1dmcdm
   8. revpfxsfxrev
   9. swrdrevpfx
3. Graph theory
   1. lfuhgr
   2. lfuhgr2
   3. lfuhgr3
   4. cplgredgex
   5. cusgredgex
   6. cusgredgex2
   7. pfxwlk
   8. revwlk
   9. revwlkb
   10. swrdwlk
   11. pthhashvtx
   12. pthisspthorcycl
   13. spthcycl
   14. usgrgt2cycl
   15. usgrcyclgt2v
   16. subgrwlk
   17. subgrtrl
   18. subgrpth
   19. subgrcycl
   20. cusgr3cyclex
   21. loop1cycl
   22. 2cycld
   23. 2cycl2d
   24. umgr2cycllem
   25. umgr2cycl
   26. Acyclic graphs