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