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