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. elrnmptd
  282. elrnmptdv
  283. elrnmpt2d
  284. dfiun3g
  285. dfiin3g
  286. dfiun3
  287. dfiin3
  288. riinint
  289. relrn0
  290. dmrnssfld
  291. dmcoss
  292. rncoss
  293. dmcosseq
  294. dmcoeq
  295. rncoeq
  296. reseq1
  297. reseq2
  298. reseq1i
  299. reseq2i
  300. reseq12i
  301. reseq1d
  302. reseq2d
  303. reseq12d
  304. nfres
  305. csbres
  306. res0
  307. dfres3
  308. opelres
  309. brres
  310. opelresi
  311. brresi
  312. opres
  313. resieq
  314. opelidres
  315. resres
  316. resundi
  317. resundir
  318. resindi
  319. resindir
  320. inres
  321. resdifcom
  322. resiun1
  323. resiun2
  324. dmres
  325. ssdmres
  326. dmresexg
  327. resss
  328. rescom
  329. ssres
  330. ssres2
  331. relres
  332. resabs1
  333. resabs1d
  334. resabs2
  335. residm
  336. resima
  337. resima2
  338. rnresss
  339. xpssres
  340. elinxp
  341. elres
  342. elsnres
  343. relssres
  344. dmressnsn
  345. eldmressnsn
  346. eldmeldmressn
  347. resdm
  348. resexg
  349. resexd
  350. resex
  351. resindm
  352. resdmdfsn
  353. resopab
  354. iss
  355. resopab2
  356. resmpt
  357. resmpt3
  358. resmptf
  359. resmptd
  360. dfres2
  361. mptss
  362. elidinxp
  363. elidinxpid
  364. elrid
  365. idinxpres
  366. idinxpresid
  367. idssxp
  368. opabresid
  369. mptresid
  370. opabresidOLD
  371. mptresidOLD
  372. dmresi
  373. restidsing
  374. iresn0n0
  375. imaeq1
  376. imaeq2
  377. imaeq1i
  378. imaeq2i
  379. imaeq1d
  380. imaeq2d
  381. imaeq12d
  382. dfima2
  383. dfima3
  384. elimag
  385. elima
  386. elima2
  387. elima3
  388. nfima
  389. nfimad
  390. imadmrn
  391. imassrn
  392. mptima
  393. imai
  394. rnresi
  395. resiima
  396. ima0
  397. 0ima
  398. csbima12
  399. imadisj
  400. cnvimass
  401. cnvimarndm
  402. imasng
  403. relimasn
  404. elrelimasn
  405. elimasn
  406. elimasng
  407. elimasni
  408. args
  409. eliniseg
  410. epini
  411. iniseg
  412. inisegn0
  413. dffr3
  414. dfse2
  415. imass1
  416. imass2
  417. ndmima
  418. relcnv
  419. relbrcnvg
  420. eliniseg2
  421. relbrcnv
  422. cotrg
  423. cotr
  424. idrefALT
  425. cnvsym
  426. intasym
  427. asymref
  428. asymref2
  429. intirr
  430. brcodir
  431. codir
  432. qfto
  433. xpidtr
  434. trin2
  435. poirr2
  436. trinxp
  437. soirri
  438. sotri
  439. son2lpi
  440. sotri2
  441. sotri3
  442. poleloe
  443. poltletr
  444. somin1
  445. somincom
  446. somin2
  447. soltmin
  448. cnvopab
  449. mptcnv
  450. cnv0
  451. cnvi
  452. cnvun
  453. cnvdif
  454. cnvin
  455. rnun
  456. rnin
  457. rniun
  458. rnuni
  459. imaundi
  460. imaundir
  461. dminss
  462. imainss
  463. inimass
  464. inimasn
  465. cnvxp
  466. xp0
  467. xpnz
  468. xpeq0
  469. xpdisj1
  470. xpdisj2
  471. xpsndisj
  472. difxp
  473. difxp1
  474. difxp2
  475. djudisj
  476. xpdifid
  477. resdisj
  478. rnxp
  479. dmxpss
  480. rnxpss
  481. rnxpid
  482. ssxpb
  483. xp11
  484. xpcan
  485. xpcan2
  486. ssrnres
  487. rninxp
  488. dminxp
  489. imainrect
  490. xpima
  491. xpima1
  492. xpima2
  493. xpimasn
  494. sossfld
  495. sofld
  496. cnvcnv3
  497. dfrel2
  498. dfrel4v
  499. dfrel4
  500. cnvcnv
  501. cnvcnv2
  502. cnvcnvss
  503. cnvrescnv
  504. cnveqb
  505. cnveq0
  506. dfrel3
  507. elid
  508. dmresv
  509. rnresv
  510. dfrn4
  511. csbrn
  512. rescnvcnv
  513. cnvcnvres
  514. imacnvcnv
  515. dmsnn0
  516. rnsnn0
  517. dmsn0
  518. cnvsn0
  519. dmsn0el
  520. relsn2
  521. dmsnopg
  522. dmsnopss
  523. dmpropg
  524. dmsnop
  525. dmprop
  526. dmtpop
  527. cnvcnvsn
  528. dmsnsnsn
  529. rnsnopg
  530. rnpropg
  531. cnvsng
  532. rnsnop
  533. op1sta
  534. cnvsn
  535. op2ndb
  536. op2nda
  537. opswap
  538. cnvresima
  539. resdm2
  540. resdmres
  541. resresdm
  542. imadmres
  543. mptpreima
  544. mptiniseg
  545. dmmpt
  546. dmmptss
  547. dmmptg
  548. relco
  549. dfco2
  550. dfco2a
  551. coundi
  552. coundir
  553. cores
  554. resco
  555. imaco
  556. rnco
  557. rnco2
  558. dmco
  559. coeq0
  560. coiun
  561. cocnvcnv1
  562. cocnvcnv2
  563. cores2
  564. co02
  565. co01
  566. coi1
  567. coi2
  568. coires1
  569. coass
  570. relcnvtrg
  571. relcnvtr
  572. relssdmrn
  573. resssxp
  574. cnvssrndm
  575. cossxp
  576. relrelss
  577. unielrel
  578. relfld
  579. relresfld
  580. relcoi2
  581. relcoi1
  582. unidmrn
  583. relcnvfld
  584. dfdm2
  585. unixp
  586. unixp0
  587. unixpid
  588. ressn
  589. cnviin
  590. cnvpo
  591. cnvso
  592. xpco
  593. xpcoid
  594. elsnxp
  595. reu3op
  596. reuop
  597. opreu2reurex
  598. opreu2reu