Metamath Proof Explorer

Table of Contents - 20.35. Mathbox for Rohan Ridenour

  1. Misc
    1. spALT
    2. elnelneqd
    3. elnelneq2d
    4. rr-spce
    5. rexlimdvaacbv
    6. rexlimddvcbvw
    7. rexlimddvcbv
    8. rr-elrnmpt3d
    9. rr-phpd
    10. suceqd
    11. tfindsd
  2. Shorter primitive equivalent of ax-groth
    1. Grothendieck universes are closed under collection
    2. Minimal universes
    3. Primitive equivalent of ax-groth