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