Metamath Proof Explorer

Table of Contents - 20.37. Mathbox for Andrew Salmon

1. Principia Mathematica * 10
   1. pm10.12
   2. pm10.14
   3. pm10.251
   4. pm10.252
   5. pm10.253
   6. albitr
   7. pm10.42
   8. pm10.52
   9. pm10.53
   10. pm10.541
   11. pm10.542
   12. pm10.55
   13. pm10.56
   14. pm10.57
2. Principia Mathematica * 11
   1. 2alanimi
   2. 2al2imi
   3. pm11.11
   4. pm11.12
   5. 19.21vv
   6. 2alim
   7. 2albi
   8. 2exim
   9. 2exbi
   10. spsbce-2
   11. 19.33-2
   12. 19.36vv
   13. 19.31vv
   14. 19.37vv
   15. 19.28vv
   16. pm11.52
   17. aaanv
   18. pm11.57
   19. pm11.58
   20. pm11.59
   21. pm11.6
   22. pm11.61
   23. pm11.62
   24. pm11.63
   25. pm11.7
   26. pm11.71
3. Predicate Calculus
   1. sbeqal1
   2. sbeqal1i
   3. sbeqal2i
   4. axc5c4c711
   5. axc5c4c711toc5
   6. axc5c4c711toc4
   7. axc5c4c711toc7
   8. axc5c4c711to11
   9. axc11next
4. Principia Mathematica * 13 and * 14
   1. pm13.13a
   2. pm13.13b
   3. pm13.14
   4. pm13.192
   5. pm13.193
   6. pm13.194
   7. pm13.195
   8. pm13.196a
   9. 2sbc6g
   10. 2sbc5g
   11. iotain
   12. iotaexeu
   13. iotasbc
   14. iotasbc2
   15. pm14.12
   16. pm14.122a
   17. pm14.122b
   18. pm14.122c
   19. pm14.123a
   20. pm14.123b
   21. pm14.123c
   22. pm14.18
   23. iotaequ
   24. iotavalb
   25. iotasbc5
   26. pm14.24
   27. iotavalsb
   28. sbiota1
   29. sbaniota
   30. eubiOLD
   31. iotasbcq
5. Set Theory
   1. elnev
   2. rusbcALT
   3. compeq
   4. compne
   5. compab
   6. conss2
   7. conss1
   8. ralbidar
   9. rexbidar
   10. dropab1
   11. dropab2
   12. ipo0
   13. ifr0
   14. ordpss
   15. fvsb
   16. fveqsb
   17. xpexb
   18. trelpss
6. Arithmetic
   1. addcomgi
7. Geometry
   1. cplusr
   2. cminusr
   3. ctimesr
   4. cptdfc
   5. crr3c
   6. cline3
   7. df-addr
   8. df-subr
   9. df-mulv
   10. addrval
   11. subrval
   12. mulvval
   13. addrfv
   14. subrfv
   15. mulvfv
   16. addrfn
   17. subrfn
   18. mulvfn
   19. addrcom
   20. df-ptdf
   21. df-rr3
   22. df-line3