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. dmmpogaOLD
87. dmmpog
88. mpoexxg
89. mpoexg
90. mpoexga
91. mpoexw
92. mpoex
93. mptmpoopabbrd
94. mptmpoopabovd
95. el2mpocsbcl
96. el2mpocl
97. fnmpoovd
98. offval22
99. brovpreldm
100. bropopvvv
101. bropfvvvvlem
102. bropfvvvv
103. ovmptss
104. relmpoopab
105. fmpoco
106. oprabco
107. oprab2co
108. df1st2
109. df2nd2
110. 1stconst
111. 2ndconst
112. dfmpo
113. mposn
114. curry1
115. curry1val
116. curry1f
117. curry2
118. curry2f
119. curry2val
120. cnvf1olem
121. cnvf1o
122. fparlem1
123. fparlem2
124. fparlem3
125. fparlem4
126. fpar
127. fsplit
128. fsplitOLD
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