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. nelpr2
  31. nelpr1
  32. nelpri
  33. prneli
  34. nelprd
  35. eldifpr
  36. rexdifpr
  37. snidg
  38. snidb
  39. snid
  40. vsnid
  41. elsn2g
  42. elsn2
  43. nelsn
  44. rabeqsn
  45. rabsssn
  46. rabeqsnd
  47. ralsnsg
  48. rexsns
  49. rexsngf
  50. ralsngf
  51. reusngf
  52. ralsng
  53. rexsng
  54. reusng
  55. 2ralsng
  56. rexreusng
  57. exsnrex
  58. ralsn
  59. rexsn
  60. elunsn
  61. elpwunsn
  62. eqoreldif
  63. eltpg
  64. eldiftp
  65. eltpi
  66. eltp
  67. el7g
  68. dftp2
  69. nfpr
  70. ifpr
  71. ralprgf
  72. rexprgf
  73. ralprg
  74. rexprg
  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. snssb
  160. snssg
  161. snss
  162. eldifsn
  163. eldifsnd
  164. ssdifsn
  165. elpwdifsn
  166. eldifsni
  167. eldifsnneq
  168. neldifsn
  169. neldifsnd
  170. rexdifsn
  171. raldifsni
  172. raldifsnb
  173. eldifvsn
  174. difsn
  175. difprsnss
  176. difprsn1
  177. difprsn2
  178. diftpsn3
  179. difpr
  180. tpprceq3
  181. tppreqb
  182. difsnb
  183. difsnpss
  184. snssi
  185. snssd
  186. difsnid
  187. eldifeldifsn
  188. pw0
  189. pwpw0
  190. snsspr1
  191. snsspr2
  192. snsstp1
  193. snsstp2
  194. snsstp3
  195. prssg
  196. prss
  197. prssi
  198. prssd
  199. prsspwg
  200. ssprss
  201. ssprsseq
  202. sssn
  203. ssunsn2
  204. ssunsn
  205. eqsn
  206. eqsnd
  207. eqsndOLD
  208. issn
  209. n0snor2el
  210. ssunpr
  211. sspr
  212. sstp
  213. tpss
  214. tpssi
  215. sneqrg
  216. sneqr
  217. snsssn
  218. mosneq
  219. sneqbg
  220. snsspw
  221. prsspw
  222. preq1b
  223. preq2b
  224. preqr1
  225. preqr2
  226. preq12b
  227. opthpr
  228. preqr1g
  229. preq12bg
  230. prneimg
  231. prneimg2
  232. prnebg
  233. pr1eqbg
  234. pr1nebg
  235. preqsnd
  236. prnesn
  237. prneprprc
  238. preqsn
  239. preq12nebg
  240. prel12g
  241. opthprneg
  242. elpreqprlem
  243. elpreqpr
  244. elpreqprb
  245. elpr2elpr
  246. dfopif
  247. dfopg
  248. dfop
  249. opeq1
  250. opeq2
  251. opeq12
  252. opeq1i
  253. opeq2i
  254. opeq12i
  255. opeq1d
  256. opeq2d
  257. opeq12d
  258. oteq1
  259. oteq2
  260. oteq3
  261. oteq1d
  262. oteq2d
  263. oteq3d
  264. oteq123d
  265. nfop
  266. nfopd
  267. csbopg
  268. opidg
  269. opid
  270. ralunsn
  271. 2ralunsn
  272. opprc
  273. opprc1
  274. opprc2
  275. oprcl
  276. pwsn
  277. pwpr
  278. pwtp
  279. pwpwpw0
  280. pwv
  281. prproe
  282. 3elpr2eq