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. elALT
13. dtruALT2
14. snelpwi
15. snelpw
16. prelpw
17. prelpwi
18. rext
19. sspwb
20. unipw
21. univ
22. pwtr
23. ssextss
24. ssext
25. nssss
26. pweqb
27. intid
28. moabex
29. rmorabex
30. euabex
31. nnullss
32. exss
33. opex
34. otex
35. elopg
36. elop
37. opi1
38. opi2
39. opeluu
40. op1stb
41. brv