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