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