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