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. 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. inxp
  160. inxpOLD
  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. csbcnv
  212. csbcnvgALT
  213. cnvco
  214. cnvuni
  215. dfdm3
  216. dfrn2
  217. dfrn3
  218. elrn2g
  219. elrng
  220. elrn2
  221. elrn
  222. ssrelrn
  223. dfdm4
  224. dfdmf
  225. csbdm
  226. eldmg
  227. eldm2g
  228. eldm
  229. eldm2
  230. dmss
  231. dmeq
  232. dmeqi
  233. dmeqd
  234. opeldmd
  235. opeldm
  236. breldm
  237. breldmg
  238. dmun
  239. dmin
  240. breldmd
  241. dmiun
  242. dmuni
  243. dmopab
  244. dmopabelb
  245. dmopab2rex
  246. dmopabss
  247. dmopab3
  248. dm0
  249. dmi
  250. dmv
  251. dmep
  252. dm0rn0
  253. dm0rn0OLD
  254. rn0
  255. rnep
  256. reldm0
  257. dmxp
  258. dmxpid
  259. dmxpin
  260. xpid11
  261. dmcnvcnv
  262. rncnvcnv
  263. elreldm
  264. rneq
  265. rneqi
  266. rneqd
  267. rnss
  268. rnssi
  269. brelrng
  270. brelrn
  271. opelrn
  272. releldm
  273. relelrn
  274. releldmb
  275. relelrnb
  276. releldmi
  277. relelrni
  278. dfrnf
  279. nfdm
  280. nfrn
  281. dmiin
  282. rnopab
  283. rnopabss
  284. rnopab3
  285. rnmpt
  286. elrnmpt
  287. elrnmpt1s
  288. elrnmpt1
  289. elrnmptg
  290. elrnmpti
  291. elrnmptd
  292. elrnmpt1d
  293. elrnmptdv
  294. elrnmpt2d
  295. nelrnmpt
  296. dfiun3g
  297. dfiin3g
  298. dfiun3
  299. dfiin3
  300. riinint
  301. relrn0
  302. dmrnssfld
  303. dmcoss
  304. dmcossOLD
  305. rncoss
  306. dmcosseq
  307. dmcosseqOLD
  308. dmcosseqOLDOLD
  309. dmcoeq
  310. rncoeq
  311. reseq1
  312. reseq2
  313. reseq1i
  314. reseq2i
  315. reseq12i
  316. reseq1d
  317. reseq2d
  318. reseq12d
  319. nfres
  320. csbres
  321. res0
  322. dfres3
  323. opelres
  324. brres
  325. opelresi
  326. brresi
  327. opres
  328. resieq
  329. opelidres
  330. resres
  331. resundi
  332. resundir
  333. resindi
  334. resindir
  335. inres
  336. resdifcom
  337. resiun1
  338. resiun2
  339. resss
  340. rescom
  341. ssres
  342. ssres2
  343. relres
  344. resabs1
  345. resabs1i
  346. resabs1d
  347. resabs2
  348. residm
  349. dmresss
  350. dmres
  351. ssdmres
  352. dmresexg
  353. resima
  354. resima2
  355. rnresss
  356. xpssres
  357. elinxp
  358. elres
  359. elsnres
  360. relssres
  361. dmressnsn
  362. eldmressnsn
  363. eldmeldmressn
  364. resdm
  365. resexg
  366. resexd
  367. resex
  368. resindm
  369. resdmdfsn
  370. reldisjun
  371. relresdm1
  372. resopab
  373. iss
  374. resopab2
  375. resmpt
  376. resmpt3
  377. resmptf
  378. resmptd
  379. dfres2
  380. mptss
  381. elimampt
  382. elidinxp
  383. elidinxpid
  384. elrid
  385. idinxpres
  386. idinxpresid
  387. idssxp
  388. opabresid
  389. mptresid
  390. dmresi
  391. restidsing
  392. iresn0n0
  393. imaeq1
  394. imaeq2
  395. imaeq1i
  396. imaeq2i
  397. imaeq1d
  398. imaeq2d
  399. imaeq12d
  400. dfima2
  401. dfima3
  402. elimag
  403. elima
  404. elima2
  405. elima3
  406. nfima
  407. nfimad
  408. imadmrn
  409. imassrn
  410. mptima
  411. mptimass
  412. imai
  413. rnresi
  414. resiima
  415. ima0
  416. 0ima
  417. csbima12
  418. imadisj
  419. imadisjlnd
  420. cnvimass
  421. cnvimarndm
  422. imasng
  423. relimasn
  424. elrelimasn
  425. elimasng1
  426. elimasn1
  427. elimasng
  428. elimasn
  429. elimasni
  430. args
  431. elinisegg
  432. eliniseg
  433. epin
  434. epini
  435. iniseg
  436. inisegn0
  437. dffr3
  438. dfse2
  439. imass1
  440. imass2
  441. ndmima
  442. relcnv
  443. relbrcnvg
  444. eliniseg2
  445. relbrcnv
  446. relco
  447. cotrg
  448. cotr
  449. idrefALT
  450. cnvsym
  451. intasym
  452. asymref
  453. asymref2
  454. intirr
  455. brcodir
  456. codir
  457. qfto
  458. xpidtr
  459. trin2
  460. poirr2
  461. trinxp
  462. soirri
  463. sotri
  464. son2lpi
  465. sotri2
  466. sotri3
  467. poleloe
  468. poltletr
  469. somin1
  470. somincom
  471. somin2
  472. soltmin
  473. cnvopab
  474. cnvopabOLD
  475. mptcnv
  476. cnv0
  477. cnv0OLD
  478. cnvi
  479. cnvun
  480. cnvdif
  481. cnvin
  482. rnun
  483. rnin
  484. rniun
  485. rnuni
  486. imaundi
  487. imaundir
  488. imadifssran
  489. cnvimassrndm
  490. dminss
  491. imainss
  492. inimass
  493. inimasn
  494. cnvxp
  495. xp0OLD
  496. xpnz
  497. xpeq0
  498. xpdisj1
  499. xpdisj2
  500. xpsndisj
  501. difxp
  502. difxp1
  503. difxp2
  504. djudisj
  505. xpdifid
  506. resdisj
  507. rnxp
  508. dmxpss
  509. rnxpss
  510. rnxpid
  511. ssxpb
  512. xp11
  513. xpcan
  514. xpcan2
  515. ssrnres
  516. rninxp
  517. dminxp
  518. imainrect
  519. xpima
  520. xpima1
  521. xpima2
  522. xpimasn
  523. sossfld
  524. sofld
  525. cnvcnv3
  526. dfrel2
  527. dfrel4v
  528. dfrel4
  529. cnvcnv
  530. cnvcnv2
  531. cnvcnvss
  532. cnvrescnv
  533. cnveqb
  534. cnveq0
  535. dfrel3
  536. elid
  537. dmresv
  538. rnresv
  539. dfrn4
  540. csbrn
  541. rescnvcnv
  542. cnvcnvres
  543. imacnvcnv
  544. dmsnn0
  545. rnsnn0
  546. dmsn0
  547. cnvsn0
  548. dmsn0el
  549. relsn2
  550. dmsnopg
  551. dmsnopss
  552. dmpropg
  553. dmsnop
  554. dmprop
  555. dmtpop
  556. cnvcnvsn
  557. dmsnsnsn
  558. rnsnopg
  559. rnpropg
  560. cnvsng
  561. rnsnop
  562. op1sta
  563. cnvsn
  564. op2ndb
  565. op2nda
  566. opswap
  567. cnvresima
  568. resdm2
  569. resdmres
  570. resresdm
  571. imadmres
  572. resdmss
  573. resdifdi
  574. resdifdir
  575. mptpreima
  576. mptiniseg
  577. dmmpt
  578. dmmptss
  579. dmmptg
  580. rnmpt0f
  581. rnmptn0
  582. dfco2
  583. dfco2a
  584. coundi
  585. coundir
  586. cores
  587. resco
  588. imaco
  589. rnco
  590. rncoOLD
  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. resssxp
  608. cnvssrndm
  609. cossxp
  610. relrelss
  611. unielrel
  612. relfld
  613. relresfld
  614. relcoi2
  615. relcoi1
  616. unidmrn
  617. relcnvfld
  618. dfdm2
  619. unixp
  620. unixp0
  621. unixpid
  622. ressn
  623. cnviin
  624. cnvpo
  625. cnvso
  626. xpco
  627. xpcoid
  628. elsnxp
  629. reu3op
  630. reuop
  631. opreu2reurex
  632. opreu2reu
  633. dfpo2
  634. csbcog
  635. snres0
  636. imaindm