Metamath Proof Explorer

Table of Contents - 2.1.18. Unordered and ordered pairs

  1. snjust
  2. csn
  3. df-sn
  4. cpr
  5. df-pr
  6. ctp
  7. df-tp
  8. cop
  9. df-op
  10. cotp
  11. df-ot
  12. sneq
  13. sneqi
  14. sneqd
  15. dfsn2
  16. elsng
  17. elsn
  18. velsn
  19. elsni
  20. elsnd
  21. rabsneq
  22. absn
  23. dfpr2
  24. dfsn2ALT
  25. elprg
  26. elpri
  27. elpr
  28. elpr2g
  29. elpr2
  30. elprn1
  31. elprn2
  32. nelpr2
  33. nelpr1
  34. nelpri
  35. prneli
  36. nelprd
  37. eldifpr
  38. rexdifpr
  39. snidg
  40. snidb
  41. snid
  42. vsnid
  43. elsn2g
  44. elsn2
  45. nelsn
  46. rabeqsn
  47. rabsssn
  48. rabeqsnd
  49. ralsnsg
  50. rexsns
  51. rexsngf
  52. ralsngf
  53. reusngf
  54. ralsng
  55. rexsng
  56. reusng
  57. 2ralsng
  58. rexreusng
  59. exsnrex
  60. ralsn
  61. rexsn
  62. elunsn
  63. elpwunsn
  64. eqoreldif
  65. eltpg
  66. eldiftp
  67. eltpi
  68. eltp
  69. el7g
  70. dftp2
  71. nfpr
  72. ifpr
  73. ralprgf
  74. rexprgf
  75. ralprg
  76. rexprg
  77. raltpg
  78. rextpg
  79. ralpr
  80. rexpr
  81. reuprg0
  82. reuprg
  83. reurexprg
  84. raltp
  85. rextp
  86. nfsn
  87. csbsng
  88. csbprg
  89. elinsn
  90. disjsn
  91. disjsn2
  92. disjpr2
  93. disjprsn
  94. disjtpsn
  95. disjtp2
  96. snprc
  97. snnzb
  98. rmosn
  99. r19.12sn
  100. rabsn
  101. rabsnifsb
  102. rabsnif
  103. rabrsn
  104. euabsn2
  105. euabsn
  106. reusn
  107. absneu
  108. rabsneu
  109. eusn
  110. rabsnt
  111. prcom
  112. preq1
  113. preq2
  114. preq12
  115. preq1i
  116. preq2i
  117. preq12i
  118. preq1d
  119. preq2d
  120. preq12d
  121. tpeq1
  122. tpeq2
  123. tpeq3
  124. tpeq1d
  125. tpeq2d
  126. tpeq3d
  127. tpeq123d
  128. tprot
  129. tpcoma
  130. tpcomb
  131. tpass
  132. qdass
  133. qdassr
  134. tpidm12
  135. tpidm13
  136. tpidm23
  137. tpidm
  138. tppreq3
  139. prid1g
  140. prid2g
  141. prid1
  142. prid2
  143. ifpprsnss
  144. prprc1
  145. prprc2
  146. prprc
  147. tpid1
  148. tpid1g
  149. tpid2
  150. tpid2g
  151. tpid3g
  152. tpid3
  153. snnzg
  154. snn0d
  155. snnz
  156. prnz
  157. prnzg
  158. tpnz
  159. tpnzd
  160. raltpd
  161. snssb
  162. snssg
  163. snss
  164. snssi
  165. snssd
  166. eldifsn
  167. eldifsnbd
  168. eldifsnd
  169. ssdifsn
  170. elpwdifsn
  171. eldifsni
  172. eldifsnneq
  173. neldifsn
  174. neldifsnd
  175. rexdifsn
  176. raldifsni
  177. raldifsnb
  178. eldifvsn
  179. difsn
  180. difprsnss
  181. difprsn1
  182. difprsn2
  183. diftpsn3
  184. difpr
  185. tpprceq3
  186. tppreqb
  187. difsnb
  188. difsnpss
  189. difsnid
  190. eldifeldifsn
  191. pw0
  192. pwpw0
  193. snsspr1
  194. snsspr2
  195. snsstp1
  196. snsstp2
  197. snsstp3
  198. prssg
  199. prss
  200. prssi
  201. prssd
  202. prsspwg
  203. ssprss
  204. ssprsseq
  205. sssn
  206. ssunsn2
  207. ssunsn
  208. eqsn
  209. eqsnd
  210. issn
  211. n0snor2el
  212. ssunpr
  213. sspr
  214. sstp
  215. tpss
  216. tpssi
  217. sneqrg
  218. sneqr
  219. snsssn
  220. mosneq
  221. sneqbg
  222. snsspw
  223. prsspw
  224. preq1b
  225. preq2b
  226. preqr1
  227. preqr2
  228. preq12b
  229. opthpr
  230. preqr1g
  231. preq12bg
  232. prneimg
  233. prneimg2
  234. prnebg
  235. pr1eqbg
  236. pr1nebg
  237. preqsnd
  238. prnesn
  239. prneprprc
  240. preqsn
  241. preq12nebg
  242. prel12g
  243. opthprneg
  244. elpreqprlem
  245. elpreqpr
  246. elpreqprb
  247. elpr2elpr
  248. dfopif
  249. dfopg
  250. dfop
  251. opeq1
  252. opeq2
  253. opeq12
  254. opeq1i
  255. opeq2i
  256. opeq12i
  257. opeq1d
  258. opeq2d
  259. opeq12d
  260. oteq1
  261. oteq2
  262. oteq3
  263. oteq1d
  264. oteq2d
  265. oteq3d
  266. oteq123d
  267. nfop
  268. nfopd
  269. csbopg
  270. opidg
  271. opid
  272. ralunsn
  273. 2ralunsn
  274. opprc
  275. opprc1
  276. opprc2
  277. oprcl
  278. pwsn
  279. pwpr
  280. pwtp
  281. pwpwpw0
  282. pwv
  283. prproe
  284. 3elpr2eq