Metamath Proof Explorer

Table of Contents - 2.4.8. First and second members of an ordered pair

1. c1st
2. c2nd
3. df-1st
4. df-2nd
5. 1stval
6. 2ndval
7. 1stnpr
8. 2ndnpr
9. 1st0
10. 2nd0
11. op1st
12. op2nd
13. op1std
14. op2ndd
15. op1stg
16. op2ndg
17. ot1stg
18. ot2ndg
19. ot3rdg
20. 1stval2
21. 2ndval2
22. oteqimp
23. fo1st
24. fo2nd
25. br1steqg
26. br2ndeqg
27. f1stres
28. f2ndres
29. fo1stres
30. fo2ndres
31. 1st2val
32. 2nd2val
33. 1stcof
34. 2ndcof
35. xp1st
36. xp2nd
37. elxp6
38. elxp7
39. eqopi
40. xp2
41. unielxp
42. 1st2nd2
43. 1st2ndb
44. xpopth
45. eqop
46. eqop2
47. op1steq
48. opreuopreu
49. el2xptp
50. el2xptp0
51. 2nd1st
52. 1st2nd
53. 1stdm
54. 2ndrn
55. 1st2ndbr
56. releldm2
57. reldm
58. releldmdifi
59. funfv1st2nd
60. funelss
61. funeldmdif
62. sbcopeq1a
63. csbopeq1a
64. dfopab2
65. dfoprab3s
66. dfoprab3
67. dfoprab4
68. dfoprab4f
69. opabex2
70. opabn1stprc
71. opiota
72. cnvoprab
73. dfxp3
74. elopabi
75. eloprabi
76. mpomptsx
77. mpompts
78. dmmpossx
79. fmpox
80. fmpo
81. fnmpo
82. fnmpoi
83. dmmpo
84. ovmpoelrn
85. dmmpoga
86. dmmpog
87. mpoexxg
88. mpoexg
89. mpoexga
90. mpoexw
91. mpoex
92. mptmpoopabbrd
93. mptmpoopabovd
94. el2mpocsbcl
95. el2mpocl
96. fnmpoovd
97. offval22
98. brovpreldm
99. bropopvvv
100. bropfvvvvlem
101. bropfvvvv
102. ovmptss
103. relmpoopab
104. fmpoco
105. oprabco
106. oprab2co
107. df1st2
108. df2nd2
109. 1stconst
110. 2ndconst
111. dfmpo
112. mposn
113. curry1
114. curry1val
115. curry1f
116. curry2
117. curry2f
118. curry2val
119. cnvf1olem
120. cnvf1o
121. fparlem1
122. fparlem2
123. fparlem3
124. fparlem4
125. fpar
126. fsplit
127. fsplitOLD
128. fsplitfpar
129. offsplitfpar
130. f2ndf
131. fo2ndf
132. f1o2ndf1
133. algrflem
134. frxp
135. xporderlem
136. poxp
137. soxp
138. wexp
139. fnwelem
140. fnwe
141. fnse
142. fvproj
143. fimaproj