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. mptmpoopabbrdOLD
96. mptmpoopabovd
97. el2mpocsbcl
98. el2mpocl
99. fnmpoovd
100. offval22
101. brovpreldm
102. bropopvvv
103. bropfvvvvlem
104. bropfvvvv
105. ovmptss
106. relmpoopab
107. fmpoco
108. oprabco
109. oprab2co
110. df1st2
111. df2nd2
112. 1stconst
113. 2ndconst
114. dfmpo
115. mposn
116. curry1
117. curry1val
118. curry1f
119. curry2
120. curry2f
121. curry2val
122. cnvf1olem
123. cnvf1o
124. fparlem1
125. fparlem2
126. fparlem3
127. fparlem4
128. fpar
129. fsplit
130. fsplitfpar
131. offsplitfpar
132. f2ndf
133. fo2ndf
134. f1o2ndf1
135. opco1
136. opco2
137. opco1i
138. frxp
139. xporderlem
140. poxp
141. soxp
142. wexp
143. fnwelem
144. fnwe
145. fnse
146. fvproj
147. fimaproj
148. ralxpes
149. ralxp3f
150. ralxp3
151. ralxp3es