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. axprlem3OLD
7. axprlem4OLD
8. axprlem5OLD
9. axprOLD
10. ax-pr
11. zfpair2
12. vsnex
13. snexg
14. snex
15. prex
16. exel
17. exexneq
18. exneq
19. dtru
20. el
21. sels
22. selsALT
23. elALT
24. snelpwg
25. snelpwi
26. snelpw
27. prelpw
28. prelpwi
29. rext
30. sspwb
31. unipw
32. univ
33. pwtr
34. ssextss
35. ssext
36. nssss
37. pweqb
38. intidg
39. moabex
40. rmorabex
41. euabex
42. nnullss
43. exss
44. opex
45. otex
46. elopg
47. elop
48. opi1
49. opi2
50. opeluu
51. op1stb
52. brv