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