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. moabexOLD
41. rmorabex
42. euabex
43. nnullss
44. exss
45. opex
46. otex
47. elopg
48. elop
49. opi1
50. opi2
51. opeluu
52. op1stb
53. brv