Metamath Proof Explorer

Table of Contents - 21.23. Mathbox for Wolf Lammen

1. wl-section-prop
2. ax-luk1
3. ax-luk2
4. ax-luk3
5. 1. Bootstrapping
   1. wl-section-boot
   2. wl-luk-imim1i
   3. wl-luk-syl
   4. wl-luk-imtrid
   5. wl-luk-pm2.18d
   6. wl-luk-con4i
   7. wl-luk-pm2.24i
   8. wl-luk-a1i
   9. wl-luk-mpi
   10. wl-luk-imim2i
   11. wl-luk-imtrdi
   12. wl-luk-ax3
   13. wl-luk-ax1
   14. wl-luk-pm2.27
   15. wl-luk-com12
   16. wl-luk-pm2.21
   17. wl-luk-con1i
   18. wl-luk-ja
   19. wl-luk-imim2
   20. wl-luk-a1d
   21. wl-luk-ax2
   22. wl-luk-id
   23. wl-luk-notnotr
   24. wl-luk-pm2.04
6. Implication chains
   1. wl-section-impchain
   2. wl-impchain-mp-x
   3. wl-impchain-mp-0
   4. wl-impchain-mp-1
   5. wl-impchain-mp-2
   6. wl-impchain-com-1.x
   7. wl-impchain-com-1.1
   8. wl-impchain-com-1.2
   9. wl-impchain-com-1.3
   10. wl-impchain-com-1.4
   11. wl-impchain-com-n.m
   12. wl-impchain-com-2.3
   13. wl-impchain-com-2.4
   14. wl-impchain-com-3.2.1
   15. wl-impchain-a1-x
   16. wl-impchain-a1-1
   17. wl-impchain-a1-2
   18. wl-impchain-a1-3
7. Theorems around the conditional operator
   1. wl-ifp-ncond1
   2. wl-ifp-ncond2
   3. wl-ifpimpr
   4. wl-ifp4impr
8. Alternative development of hadd, cadd
   1. wl-df-3xor
   2. wl-df3xor2
   3. wl-df3xor3
   4. wl-3xortru
   5. wl-3xorfal
   6. wl-3xorbi
   7. wl-3xorbi2
   8. wl-3xorbi123d
   9. wl-3xorbi123i
   10. wl-3xorrot
   11. wl-3xorcoma
   12. wl-3xorcomb
   13. wl-3xornot1
   14. wl-3xornot
   15. wl-1xor
   16. wl-2xor
   17. wl-df-3mintru2
   18. wl-df2-3mintru2
   19. wl-df3-3mintru2
   20. wl-df4-3mintru2
   21. wl-1mintru1
   22. wl-1mintru2
   23. wl-2mintru1
   24. wl-2mintru2
   25. wl-df3maxtru1
9. An alternative axiom ~ ax-13
   1. ax-wl-13v
   2. wl-ax13lem1
10. Bootstrapping set theory with classes
    1. wl-cleq-0
    2. wl-cleq-1
    3. wl-cleq-2
    4. wl-cleq-3
    5. wl-cleq-4
    6. wl-cleq-5
    7. wl-cleq-6
    8. ax-wl-cleq
    9. ax-wl-clel
    10. wl-df-clab
    11. wl-isseteq
    12. wl-ax12v2cl
11. Other stuff
    1. wl-mps
    2. wl-syls1
    3. wl-syls2
    4. wl-embant
    5. wl-orel12
    6. wl-cases2-dnf
    7. wl-cbvmotv
    8. wl-moteq
    9. wl-motae
    10. wl-moae
    11. wl-euae
    12. wl-nax6im
    13. wl-hbae1
    14. wl-naevhba1v
    15. wl-spae
    16. wl-speqv
    17. wl-19.8eqv
    18. wl-19.2reqv
    19. wl-nfalv
    20. wl-nfimf1
    21. wl-nfae1
    22. wl-nfnae1
    23. wl-aetr
    24. wl-axc11r
    25. wl-dral1d
    26. wl-cbvalnaed
    27. wl-cbvalnae
    28. wl-exeq
    29. wl-aleq
    30. wl-nfeqfb
    31. wl-nfs1t
    32. wl-equsalvw
    33. wl-equsald
    34. wl-equsaldv
    35. wl-equsal
    36. wl-equsal1t
    37. wl-equsalcom
    38. wl-equsal1i
    39. wl-sbid2ft
    40. wl-cbvalsbi
    41. wl-sbrimt
    42. wl-sblimt
    43. wl-sb9v
    44. wl-sb8ft
    45. wl-sb8eft
    46. wl-sb8t
    47. wl-sb8et
    48. wl-sbhbt
    49. wl-sbnf1
    50. wl-equsb3
    51. wl-equsb4
    52. wl-2sb6d
    53. wl-sbcom2d-lem1
    54. wl-sbcom2d-lem2
    55. wl-sbcom2d
    56. wl-sbalnae
    57. wl-sbal1
    58. wl-sbal2
    59. wl-2spsbbi
    60. wl-lem-exsb
    61. wl-lem-nexmo
    62. wl-lem-moexsb
    63. wl-alanbii
    64. wl-mo2df
    65. wl-mo2tf
    66. wl-eudf
    67. wl-eutf
    68. wl-euequf
    69. wl-mo2t
    70. wl-mo3t
    71. wl-nfsbtv
    72. wl-sb8eut
    73. wl-sb8eutv
    74. wl-sb8mot
    75. wl-sb8motv
    76. wl-issetft
    77. wl-axc11rc11
    78. ax-wl-11v
    79. wl-ax11-lem1
    80. wl-ax11-lem2
    81. wl-ax11-lem3
    82. wl-ax11-lem4
    83. wl-ax11-lem5
    84. wl-ax11-lem6
    85. wl-ax11-lem7
    86. wl-ax11-lem8
    87. wl-ax11-lem9
    88. wl-ax11-lem10
    89. wl-clabv
    90. wl-dfclab
    91. wl-clabtv
    92. wl-clabt