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. eldifsn
  165. eldifsnd
  166. ssdifsn
  167. elpwdifsn
  168. eldifsni
  169. eldifsnneq
  170. neldifsn
  171. neldifsnd
  172. rexdifsn
  173. raldifsni
  174. raldifsnb
  175. eldifvsn
  176. difsn
  177. difprsnss
  178. difprsn1
  179. difprsn2
  180. diftpsn3
  181. difpr
  182. tpprceq3
  183. tppreqb
  184. difsnb
  185. difsnpss
  186. snssi
  187. snssd
  188. difsnid
  189. eldifeldifsn
  190. pw0
  191. pwpw0
  192. snsspr1
  193. snsspr2
  194. snsstp1
  195. snsstp2
  196. snsstp3
  197. prssg
  198. prss
  199. prssi
  200. prssd
  201. prsspwg
  202. ssprss
  203. ssprsseq
  204. sssn
  205. ssunsn2
  206. ssunsn
  207. eqsn
  208. eqsnd
  209. eqsndOLD
  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