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