Metamath Proof Explorer

Table of Contents - 2.3.2. Derive the Axiom of Pairing

  1. axprlem1
  2. axprlem2
  3. axprlem3
  4. axprlem4
  5. axpr
  6. axprlem1OLD
  7. axprlem3OLD
  8. axprlem4OLD
  9. axprlem5OLD
  10. axprOLD
  11. ax-pr
  12. zfpair2
  13. vsnex
  14. axprglem
  15. axprg
  16. prex
  17. snex
  18. snexg
  19. snexgALT
  20. snexOLD
  21. prexOLD
  22. exel
  23. exexneq
  24. exneq
  25. dtru
  26. el
  27. elOLD
  28. sels
  29. selsALT
  30. elALT
  31. snelpwg
  32. snelpwi
  33. snelpw
  34. prelpw
  35. prelpwi
  36. rext
  37. sspwb
  38. unipw
  39. univ
  40. pwtr
  41. ssextss
  42. ssext
  43. nssss
  44. pweqb
  45. intidg
  46. moabex
  47. moabexOLD
  48. rmorabex
  49. euabex
  50. nnullss
  51. exss
  52. opex
  53. opexOLD
  54. otex
  55. elopg
  56. elop
  57. opi1
  58. opi2
  59. opeluu
  60. op1stb
  61. brv