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. el2xpss
52. 2nd1st
53. 1st2nd
54. 1stdm
55. 2ndrn
56. 1st2ndbr
57. releldm2
58. reldm
59. releldmdifi
60. funfv1st2nd
61. funelss
62. funeldmdif
63. sbcopeq1a
64. csbopeq1a
65. sbcoteq1a
66. dfopab2
67. dfoprab3s
68. dfoprab3
69. dfoprab4
70. dfoprab4f
71. opabex2
72. opabn1stprc
73. opiota
74. cnvoprab
75. dfxp3
76. elopabi
77. eloprabi
78. mpomptsx
79. mpompts
80. dmmpossx
81. fmpox
82. fmpo
83. fnmpo
84. fnmpoi
85. dmmpo
86. ovmpoelrn
87. dmmpoga
88. dmmpog
89. mpoexxg
90. mpoexg
91. mpoexga
92. mpoexw
93. mpoex
94. mptmpoopabbrd
95. mptmpoopabovd
96. el2mpocsbcl
97. el2mpocl
98. fnmpoovd
99. offval22
100. brovpreldm
101. bropopvvv
102. bropfvvvvlem
103. bropfvvvv
104. ovmptss
105. relmpoopab
106. fmpoco
107. oprabco
108. oprab2co
109. df1st2
110. df2nd2
111. 1stconst
112. 2ndconst
113. dfmpo
114. mposn
115. curry1
116. curry1val
117. curry1f
118. curry2
119. curry2f
120. curry2val
121. cnvf1olem
122. cnvf1o
123. fparlem1
124. fparlem2
125. fparlem3
126. fparlem4
127. fpar
128. fsplit
129. fsplitfpar
130. offsplitfpar
131. f2ndf
132. fo2ndf
133. f1o2ndf1
134. opco1
135. opco2
136. opco1i
137. frxp
138. xporderlem
139. poxp
140. soxp
141. wexp
142. fnwelem
143. fnwe
144. fnse
145. fvproj
146. fimaproj
147. ralxpes
148. ralxp3f
149. ralxp3
150. ralxp3es