Metamath Proof Explorer

Table of Contents - 2.3.2. Derive the Axiom of Pairing

1. axprlem1
2. axprlem2
3. axprlem3
4. axprlem4
5. axprlem5
6. axpr
7. ax-pr
8. zfpair2
9. snex
10. prex
11. sels
12. el
13. elALT
14. dtru
15. snelpwi
16. snelpw
17. prelpw
18. prelpwi
19. rext
20. sspwb
21. unipw
22. univ
23. pwtr
24. ssextss
25. ssext
26. nssss
27. pweqb
28. intid
29. moabex
30. rmorabex
31. euabex
32. nnullss
33. exss
34. opex
35. otex
36. elopg
37. elop
38. opi1
39. opi2
40. opeluu
41. op1stb
42. brv