Metamath Proof Explorer

Table of Contents - 21.12. Mathbox for Scott Fenton

1. ZFC Axioms in primitive form
   1. axextprim
   2. axrepprim
   3. axunprim
   4. axpowprim
   5. axregprim
   6. axinfprim
   7. axacprim
2. Untangled classes
   1. untelirr
   2. untuni
   3. untsucf
   4. unt0
   5. untint
   6. efrunt
   7. untangtr
3. Extra propositional calculus theorems
   1. 3jaodd
   2. 3orit
   3. biimpexp
4. Misc. Useful Theorems
   1. nepss
   2. 3ccased
   3. dfso3
   4. brtpid1
   5. brtpid2
   6. brtpid3
   7. iota5f
   8. jath
   9. xpab
   10. nnuni
5. Properties of real and complex numbers
   1. sqdivzi
   2. supfz
   3. inffz
   4. fz0n
   5. shftvalg
   6. divcnvlin
   7. climlec3
   8. iexpire
   9. bcneg1
   10. bcm1nt
   11. bcprod
   12. bccolsum
6. Infinite products
   1. iprodefisumlem
   2. iprodefisum
   3. iprodgam
7. Factorial limits
   1. faclimlem1
   2. faclimlem2
   3. faclimlem3
   4. faclim
   5. iprodfac
   6. faclim2
8. Greatest common divisor and divisibility
   1. gcd32
   2. gcdabsorb
9. Properties of relationships
   1. dftr6
   2. coep
   3. coepr
   4. dffr5
   5. dfso2
   6. br8
   7. br6
   8. br4
   9. cnvco1
   10. cnvco2
   11. eldm3
   12. elrn3
   13. pocnv
   14. socnv
   15. elintfv
10. Properties of functions and mappings
    1. funpsstri
    2. fundmpss
    3. funsseq
    4. fununiq
    5. funbreq
    6. br1steq
    7. br2ndeq
    8. dfdm5
    9. dfrn5
    10. opelco3
    11. elima4
    12. fv1stcnv
    13. fv2ndcnv
11. Ordinal numbers
    1. elpotr
    2. dford5reg
    3. dfon2lem1
    4. dfon2lem2
    5. dfon2lem3
    6. dfon2lem4
    7. dfon2lem5
    8. dfon2lem6
    9. dfon2lem7
    10. dfon2lem8
    11. dfon2lem9
    12. dfon2
    13. rdgprc0
    14. rdgprc
    15. dfrdg2
    16. dfrdg3
12. Defined equality axioms
    1. axextdfeq
    2. ax8dfeq
    3. axextdist
    4. axextbdist
    5. 19.12b
    6. exnel
    7. distel
    8. axextndbi
13. Hypothesis builders
    1. hbntg
    2. hbimtg
    3. hbaltg
    4. hbng
    5. hbimg
14. Well-founded zero, successor, and limits
    1. cwsuc
    2. cwlim
    3. df-wsuc
    4. df-wlim
    5. wsuceq123
    6. wsuceq1
    7. wsuceq2
    8. wsuceq3
    9. nfwsuc
    10. wlimeq12
    11. wlimeq1
    12. wlimeq2
    13. nfwlim
    14. elwlim
    15. wzel
    16. wsuclem
    17. wsucex
    18. wsuccl
    19. wsuclb
    20. wlimss
15. Quantifier-free definitions
    1. ctxp
    2. cpprod
    3. csset
    4. ctrans
    5. cbigcup
    6. cfix
    7. climits
    8. cfuns
    9. csingle
    10. csingles
    11. cimage
    12. ccart
    13. cimg
    14. cdomain
    15. crange
    16. capply
    17. ccup
    18. ccap
    19. csuccf
    20. cfunpart
    21. cfullfn
    22. crestrict
    23. cub
    24. clb
    25. df-txp
    26. df-pprod
    27. df-sset
    28. df-trans
    29. df-bigcup
    30. df-fix
    31. df-limits
    32. df-funs
    33. df-singleton
    34. df-singles
    35. df-image
    36. df-cart
    37. df-img
    38. df-domain
    39. df-range
    40. df-cup
    41. df-cap
    42. df-restrict
    43. df-succf
    44. df-apply
    45. df-funpart
    46. df-fullfun
    47. df-ub
    48. df-lb
    49. txpss3v
    50. txprel
    51. brtxp
    52. brtxp2
    53. dfpprod2
    54. pprodcnveq
    55. pprodss4v
    56. brpprod
    57. brpprod3a
    58. brpprod3b
    59. relsset
    60. brsset
    61. idsset
    62. eltrans
    63. dfon3
    64. dfon4
    65. brtxpsd
    66. brtxpsd2
    67. brtxpsd3
    68. relbigcup
    69. brbigcup
    70. dfbigcup2
    71. fobigcup
    72. fnbigcup
    73. fvbigcup
    74. elfix
    75. elfix2
    76. dffix2
    77. fixssdm
    78. fixssrn
    79. fixcnv
    80. fixun
    81. ellimits
    82. limitssson
    83. dfom5b
    84. sscoid
    85. dffun10
    86. elfuns
    87. elfunsg
    88. brsingle
    89. elsingles
    90. fnsingle
    91. fvsingle
    92. dfsingles2
    93. snelsingles
    94. dfiota3
    95. dffv5
    96. unisnif
    97. brimage
    98. brimageg
    99. funimage
    100. fnimage
    101. imageval
    102. fvimage
    103. brcart
    104. brdomain
    105. brrange
    106. brdomaing
    107. brrangeg
    108. brimg
    109. brapply
    110. brcup
    111. brcap
    112. lemsuccf
    113. brsuccf
    114. dfsuccf2
    115. funpartlem
    116. funpartfun
    117. funpartss
    118. funpartfv
    119. fullfunfnv
    120. fullfunfv
    121. brfullfun
    122. brrestrict
    123. dfrecs2
    124. dfrdg4
    125. dfint3
    126. imagesset
    127. brub
    128. brlb
16. Alternate ordered pairs
    1. caltop
    2. caltxp
    3. df-altop
    4. df-altxp
    5. altopex
    6. altopthsn
    7. altopeq12
    8. altopeq1
    9. altopeq2
    10. altopth1
    11. altopth2
    12. altopthg
    13. altopthbg
    14. altopth
    15. altopthb
    16. altopthc
    17. altopthd
    18. altxpeq1
    19. altxpeq2
    20. elaltxp
    21. altopelaltxp
    22. altxpsspw
    23. altxpexg
    24. rankaltopb
    25. nfaltop
    26. sbcaltop
17. Geometry in the Euclidean space
    1. Congruence properties
    2. Betweenness properties
    3. Segment Transportation
    4. Properties relating betweenness and congruence
    5. Connectivity of betweenness
    6. Segment less than or equal to
    7. Outside-of relationship
    8. Lines and Rays
18. Forward difference
    1. cfwddif
    2. df-fwddif
    3. cfwddifn
    4. df-fwddifn
    5. fwddifval
    6. fwddifnval
    7. fwddifn0
    8. fwddifnp1
19. Rank theorems
    1. rankung
    2. ranksng
    3. rankelg
    4. rankpwg
    5. rank0
    6. rankeq1o
20. Hereditarily Finite Sets
    1. chf
    2. df-hf
    3. elhf
    4. elhf2
    5. elhf2g
    6. 0hf
    7. hfun
    8. hfsn
    9. hfadj
    10. hfelhf
    11. hftr
    12. hfext
    13. hfuni
    14. hfpw
    15. hfninf