Metamath Proof Explorer

Table of Contents - 2.3.10. Relations

  1. cxp
  2. ccnv
  3. cdm
  4. crn
  5. cres
  6. cima
  7. ccom
  8. wrel
  9. df-xp
  10. df-rel
  11. df-cnv
  12. df-co
  13. df-dm
  14. df-rn
  15. df-res
  16. df-ima
  17. xpeq1
  18. xpss12
  19. xpss
  20. inxpssres
  21. relxp
  22. xpss1
  23. xpss2
  24. xpeq2
  25. elxpi
  26. elxp
  27. elxp2
  28. xpeq12
  29. xpeq1i
  30. xpeq2i
  31. xpeq12i
  32. xpeq1d
  33. xpeq2d
  34. xpeq12d
  35. sqxpeqd
  36. nfxp
  37. 0nelxp
  38. 0nelelxp
  39. opelxp
  40. opelxpi
  41. opelxpd
  42. opelvv
  43. opelvvg
  44. opelxp1
  45. opelxp2
  46. otelxp1
  47. otel3xp
  48. opabssxpd
  49. rabxp
  50. brxp
  51. pwvrel
  52. pwvabrel
  53. brrelex12
  54. brrelex1
  55. brrelex2
  56. brrelex12i
  57. brrelex1i
  58. brrelex2i
  59. nprrel12
  60. nprrel
  61. 0nelrel0
  62. 0nelrel
  63. fconstmpt
  64. vtoclr
  65. opthprc
  66. brel
  67. elxp3
  68. opeliunxp
  69. xpundi
  70. xpundir
  71. xpiundi
  72. xpiundir
  73. iunxpconst
  74. xpun
  75. elvv
  76. elvvv
  77. elvvuni
  78. brinxp2
  79. brinxp
  80. opelinxp
  81. poinxp
  82. soinxp
  83. frinxp
  84. seinxp
  85. weinxp
  86. posn
  87. sosn
  88. frsn
  89. wesn
  90. elopaelxp
  91. bropaex12
  92. opabssxp
  93. brab2a
  94. optocl
  95. 2optocl
  96. 3optocl
  97. opbrop
  98. 0xp
  99. csbxp
  100. releq
  101. releqi
  102. releqd
  103. nfrel
  104. sbcrel
  105. relss
  106. ssrel
  107. eqrel
  108. ssrel2
  109. relssi
  110. relssdv
  111. eqrelriv
  112. eqrelriiv
  113. eqbrriv
  114. eqrelrdv
  115. eqbrrdv
  116. eqbrrdiv
  117. eqrelrdv2
  118. ssrelrel
  119. eqrelrel
  120. elrel
  121. rel0
  122. nrelv
  123. relsng
  124. relsnb
  125. relsnopg
  126. relsn
  127. relsnop
  128. copsex2gb
  129. copsex2ga
  130. elopaba
  131. xpsspw
  132. unixpss
  133. relun
  134. relin1
  135. relin2
  136. relinxp
  137. reldif
  138. reliun
  139. reliin
  140. reluni
  141. relint
  142. relopabiv
  143. relopabv
  144. relopabi
  145. relopabiALT
  146. relopab
  147. mptrel
  148. reli
  149. rele
  150. opabid2
  151. inopab
  152. difopab
  153. inxp
  154. xpindi
  155. xpindir
  156. xpiindi
  157. xpriindi
  158. eliunxp
  159. opeliunxp2
  160. raliunxp
  161. rexiunxp
  162. ralxp
  163. rexxp
  164. exopxfr
  165. exopxfr2
  166. djussxp
  167. ralxpf
  168. rexxpf
  169. iunxpf
  170. opabbi2dv
  171. relop
  172. ideqg
  173. ideq
  174. ididg
  175. issetid
  176. coss1
  177. coss2
  178. coeq1
  179. coeq2
  180. coeq1i
  181. coeq2i
  182. coeq1d
  183. coeq2d
  184. coeq12i
  185. coeq12d
  186. nfco
  187. brcog
  188. opelco2g
  189. brcogw
  190. eqbrrdva
  191. brco
  192. opelco
  193. cnvss
  194. cnveq
  195. cnveqi
  196. cnveqd
  197. elcnv
  198. elcnv2
  199. nfcnv
  200. brcnvg
  201. opelcnvg
  202. opelcnv
  203. brcnv
  204. csbcnv
  205. csbcnvgALT
  206. cnvco
  207. cnvuni
  208. dfdm3
  209. dfrn2
  210. dfrn3
  211. elrn2g
  212. elrng
  213. elrn2
  214. elrn
  215. ssrelrn
  216. dfdm4
  217. dfdmf
  218. csbdm
  219. eldmg
  220. eldm2g
  221. eldm
  222. eldm2
  223. dmss
  224. dmeq
  225. dmeqi
  226. dmeqd
  227. opeldmd
  228. opeldm
  229. breldm
  230. breldmg
  231. dmun
  232. dmin
  233. breldmd
  234. dmiun
  235. dmuni
  236. dmopab
  237. dmopabelb
  238. dmopab2rex
  239. dmopabss
  240. dmopab3
  241. dm0
  242. dmi
  243. dmv
  244. dmep
  245. domepOLD
  246. dm0rn0
  247. rn0
  248. rnep
  249. reldm0
  250. dmxp
  251. dmxpid
  252. dmxpin
  253. xpid11
  254. dmcnvcnv
  255. rncnvcnv
  256. elreldm
  257. rneq
  258. rneqi
  259. rneqd
  260. rnss
  261. rnssi
  262. brelrng
  263. brelrn
  264. opelrn
  265. releldm
  266. relelrn
  267. releldmb
  268. relelrnb
  269. releldmi
  270. relelrni
  271. dfrnf
  272. nfdm
  273. nfrn
  274. dmiin
  275. rnopab
  276. rnmpt
  277. elrnmpt
  278. elrnmpt1s
  279. elrnmpt1
  280. elrnmptg
  281. elrnmpti
  282. elrnmptd
  283. elrnmptdv
  284. elrnmpt2d
  285. dfiun3g
  286. dfiin3g
  287. dfiun3
  288. dfiin3
  289. riinint
  290. relrn0
  291. dmrnssfld
  292. dmcoss
  293. rncoss
  294. dmcosseq
  295. dmcoeq
  296. rncoeq
  297. reseq1
  298. reseq2
  299. reseq1i
  300. reseq2i
  301. reseq12i
  302. reseq1d
  303. reseq2d
  304. reseq12d
  305. nfres
  306. csbres
  307. res0
  308. dfres3
  309. opelres
  310. brres
  311. opelresi
  312. brresi
  313. opres
  314. resieq
  315. opelidres
  316. resres
  317. resundi
  318. resundir
  319. resindi
  320. resindir
  321. inres
  322. resdifcom
  323. resiun1
  324. resiun2
  325. dmres
  326. ssdmres
  327. dmresexg
  328. resss
  329. rescom
  330. ssres
  331. ssres2
  332. relres
  333. resabs1
  334. resabs1d
  335. resabs2
  336. residm
  337. resima
  338. resima2
  339. rnresss
  340. xpssres
  341. elinxp
  342. elres
  343. elsnres
  344. relssres
  345. dmressnsn
  346. eldmressnsn
  347. eldmeldmressn
  348. resdm
  349. resexg
  350. resexd
  351. resex
  352. resindm
  353. resdmdfsn
  354. resopab
  355. iss
  356. resopab2
  357. resmpt
  358. resmpt3
  359. resmptf
  360. resmptd
  361. dfres2
  362. mptss
  363. elidinxp
  364. elidinxpid
  365. elrid
  366. idinxpres
  367. idinxpresid
  368. idssxp
  369. opabresid
  370. mptresid
  371. opabresidOLD
  372. mptresidOLD
  373. dmresi
  374. restidsing
  375. iresn0n0
  376. imaeq1
  377. imaeq2
  378. imaeq1i
  379. imaeq2i
  380. imaeq1d
  381. imaeq2d
  382. imaeq12d
  383. dfima2
  384. dfima3
  385. elimag
  386. elima
  387. elima2
  388. elima3
  389. nfima
  390. nfimad
  391. imadmrn
  392. imassrn
  393. mptima
  394. imai
  395. rnresi
  396. resiima
  397. ima0
  398. 0ima
  399. csbima12
  400. imadisj
  401. cnvimass
  402. cnvimarndm
  403. imasng
  404. relimasn
  405. elrelimasn
  406. elimasng1
  407. elimasn1
  408. elimasng
  409. elimasn
  410. elimasngOLD
  411. elimasni
  412. args
  413. elinisegg
  414. eliniseg
  415. epin
  416. epini
  417. iniseg
  418. inisegn0
  419. dffr3
  420. dfse2
  421. imass1
  422. imass2
  423. ndmima
  424. relcnv
  425. relbrcnvg
  426. eliniseg2
  427. relbrcnv
  428. cotrg
  429. cotr
  430. idrefALT
  431. cnvsym
  432. intasym
  433. asymref
  434. asymref2
  435. intirr
  436. brcodir
  437. codir
  438. qfto
  439. xpidtr
  440. trin2
  441. poirr2
  442. trinxp
  443. soirri
  444. sotri
  445. son2lpi
  446. sotri2
  447. sotri3
  448. poleloe
  449. poltletr
  450. somin1
  451. somincom
  452. somin2
  453. soltmin
  454. cnvopab
  455. mptcnv
  456. cnv0
  457. cnvi
  458. cnvun
  459. cnvdif
  460. cnvin
  461. rnun
  462. rnin
  463. rniun
  464. rnuni
  465. imaundi
  466. imaundir
  467. cnvimassrndm
  468. dminss
  469. imainss
  470. inimass
  471. inimasn
  472. cnvxp
  473. xp0
  474. xpnz
  475. xpeq0
  476. xpdisj1
  477. xpdisj2
  478. xpsndisj
  479. difxp
  480. difxp1
  481. difxp2
  482. djudisj
  483. xpdifid
  484. resdisj
  485. rnxp
  486. dmxpss
  487. rnxpss
  488. rnxpid
  489. ssxpb
  490. xp11
  491. xpcan
  492. xpcan2
  493. ssrnres
  494. rninxp
  495. dminxp
  496. imainrect
  497. xpima
  498. xpima1
  499. xpima2
  500. xpimasn
  501. sossfld
  502. sofld
  503. cnvcnv3
  504. dfrel2
  505. dfrel4v
  506. dfrel4
  507. cnvcnv
  508. cnvcnv2
  509. cnvcnvss
  510. cnvrescnv
  511. cnveqb
  512. cnveq0
  513. dfrel3
  514. elid
  515. dmresv
  516. rnresv
  517. dfrn4
  518. csbrn
  519. rescnvcnv
  520. cnvcnvres
  521. imacnvcnv
  522. dmsnn0
  523. rnsnn0
  524. dmsn0
  525. cnvsn0
  526. dmsn0el
  527. relsn2
  528. dmsnopg
  529. dmsnopss
  530. dmpropg
  531. dmsnop
  532. dmprop
  533. dmtpop
  534. cnvcnvsn
  535. dmsnsnsn
  536. rnsnopg
  537. rnpropg
  538. cnvsng
  539. rnsnop
  540. op1sta
  541. cnvsn
  542. op2ndb
  543. op2nda
  544. opswap
  545. cnvresima
  546. resdm2
  547. resdmres
  548. resresdm
  549. imadmres
  550. resdmss
  551. resdifdi
  552. resdifdir
  553. mptpreima
  554. mptiniseg
  555. dmmpt
  556. dmmptss
  557. dmmptg
  558. rnmpt0f
  559. rnmptn0
  560. relco
  561. dfco2
  562. dfco2a
  563. coundi
  564. coundir
  565. cores
  566. resco
  567. imaco
  568. rnco
  569. rnco2
  570. dmco
  571. coeq0
  572. coiun
  573. cocnvcnv1
  574. cocnvcnv2
  575. cores2
  576. co02
  577. co01
  578. coi1
  579. coi2
  580. coires1
  581. coass
  582. relcnvtrg
  583. relcnvtr
  584. relssdmrn
  585. resssxp
  586. cnvssrndm
  587. cossxp
  588. relrelss
  589. unielrel
  590. relfld
  591. relresfld
  592. relcoi2
  593. relcoi1
  594. unidmrn
  595. relcnvfld
  596. dfdm2
  597. unixp
  598. unixp0
  599. unixpid
  600. ressn
  601. cnviin
  602. cnvpo
  603. cnvso
  604. xpco
  605. xpcoid
  606. elsnxp
  607. reu3op
  608. reuop
  609. opreu2reurex
  610. opreu2reu
  611. dfpo2
  612. csbcog