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. xpundi
72. xpundir
73. xpiundi
74. xpiundir
75. iunxpconst
76. xpun
77. elvv
78. elvvv
79. elvvuni
80. brinxp2
81. brinxp
82. opelinxp
83. poinxp
84. soinxp
85. frinxp
86. seinxp
87. weinxp
88. posn
89. sosn
90. frsn
91. wesn
92. elopaelxp
93. elopaelxpOLD
94. bropaex12
95. opabssxp
96. brab2a
97. optocl
98. 2optocl
99. 3optocl
100. opbrop
101. 0xp
102. csbxp
103. releq
104. releqi
105. releqd
106. nfrel
107. sbcrel
108. relss
109. ssrel
110. ssrelOLD
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. difopabOLD
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. rn0
254. rnep
255. reldm0
256. dmxp
257. dmxpid
258. dmxpin
259. xpid11
260. dmcnvcnv
261. rncnvcnv
262. elreldm
263. rneq
264. rneqi
265. rneqd
266. rnss
267. rnssi
268. brelrng
269. brelrn
270. opelrn
271. releldm
272. relelrn
273. releldmb
274. relelrnb
275. releldmi
276. relelrni
277. dfrnf
278. nfdm
279. nfrn
280. dmiin
281. rnopab
282. rnmpt
283. elrnmpt
284. elrnmpt1s
285. elrnmpt1
286. elrnmptg
287. elrnmpti
288. elrnmptd
289. elrnmpt1d
290. elrnmptdv
291. elrnmpt2d
292. dfiun3g
293. dfiin3g
294. dfiun3
295. dfiin3
296. riinint
297. relrn0
298. dmrnssfld
299. dmcoss
300. rncoss
301. dmcosseq
302. dmcoeq
303. rncoeq
304. reseq1
305. reseq2
306. reseq1i
307. reseq2i
308. reseq12i
309. reseq1d
310. reseq2d
311. reseq12d
312. nfres
313. csbres
314. res0
315. dfres3
316. opelres
317. brres
318. opelresi
319. brresi
320. opres
321. resieq
322. opelidres
323. resres
324. resundi
325. resundir
326. resindi
327. resindir
328. inres
329. resdifcom
330. resiun1
331. resiun2
332. resss
333. rescom
334. ssres
335. ssres2
336. relres
337. resabs1
338. resabs1d
339. resabs2
340. residm
341. dmresss
342. dmres
343. ssdmres
344. dmresexg
345. resima
346. resima2
347. rnresss
348. xpssres
349. elinxp
350. elres
351. elsnres
352. relssres
353. dmressnsn
354. eldmressnsn
355. eldmeldmressn
356. resdm
357. resexg
358. resexd
359. resex
360. resindm
361. resdmdfsn
362. reldisjun
363. relresdm1
364. resopab
365. iss
366. resopab2
367. resmpt
368. resmpt3
369. resmptf
370. resmptd
371. dfres2
372. mptss
373. elidinxp
374. elidinxpid
375. elrid
376. idinxpres
377. idinxpresid
378. idssxp
379. opabresid
380. mptresid
381. dmresi
382. restidsing
383. iresn0n0
384. imaeq1
385. imaeq2
386. imaeq1i
387. imaeq2i
388. imaeq1d
389. imaeq2d
390. imaeq12d
391. dfima2
392. dfima3
393. elimag
394. elima
395. elima2
396. elima3
397. nfima
398. nfimad
399. imadmrn
400. imassrn
401. mptima
402. mptimass
403. imai
404. rnresi
405. resiima
406. ima0
407. 0ima
408. csbima12
409. imadisj
410. imadisjlnd
411. cnvimass
412. cnvimarndm
413. imasng
414. relimasn
415. elrelimasn
416. elimasng1
417. elimasn1
418. elimasng
419. elimasn
420. elimasngOLD
421. elimasni
422. args
423. elinisegg
424. eliniseg
425. epin
426. epini
427. iniseg
428. inisegn0
429. dffr3
430. dfse2
431. imass1
432. imass2
433. ndmima
434. relcnv
435. relbrcnvg
436. eliniseg2
437. relbrcnv
438. relco
439. cotrg
440. cotrgOLD
441. cotrgOLDOLD
442. cotr
443. idrefALT
444. cnvsym
445. cnvsymOLD
446. cnvsymOLDOLD
447. intasym
448. asymref
449. asymref2
450. intirr
451. brcodir
452. codir
453. qfto
454. xpidtr
455. trin2
456. poirr2
457. trinxp
458. soirri
459. sotri
460. son2lpi
461. sotri2
462. sotri3
463. poleloe
464. poltletr
465. somin1
466. somincom
467. somin2
468. soltmin
469. cnvopab
470. mptcnv
471. cnv0
472. cnvi
473. cnvun
474. cnvdif
475. cnvin
476. rnun
477. rnin
478. rniun
479. rnuni
480. imaundi
481. imaundir
482. cnvimassrndm
483. dminss
484. imainss
485. inimass
486. inimasn
487. cnvxp
488. xp0
489. xpnz
490. xpeq0
491. xpdisj1
492. xpdisj2
493. xpsndisj
494. difxp
495. difxp1
496. difxp2
497. djudisj
498. xpdifid
499. resdisj
500. rnxp
501. dmxpss
502. rnxpss
503. rnxpid
504. ssxpb
505. xp11
506. xpcan
507. xpcan2
508. ssrnres
509. rninxp
510. dminxp
511. imainrect
512. xpima
513. xpima1
514. xpima2
515. xpimasn
516. sossfld
517. sofld
518. cnvcnv3
519. dfrel2
520. dfrel4v
521. dfrel4
522. cnvcnv
523. cnvcnv2
524. cnvcnvss
525. cnvrescnv
526. cnveqb
527. cnveq0
528. dfrel3
529. elid
530. dmresv
531. rnresv
532. dfrn4
533. csbrn
534. rescnvcnv
535. cnvcnvres
536. imacnvcnv
537. dmsnn0
538. rnsnn0
539. dmsn0
540. cnvsn0
541. dmsn0el
542. relsn2
543. dmsnopg
544. dmsnopss
545. dmpropg
546. dmsnop
547. dmprop
548. dmtpop
549. cnvcnvsn
550. dmsnsnsn
551. rnsnopg
552. rnpropg
553. cnvsng
554. rnsnop
555. op1sta
556. cnvsn
557. op2ndb
558. op2nda
559. opswap
560. cnvresima
561. resdm2
562. resdmres
563. resresdm
564. imadmres
565. resdmss
566. resdifdi
567. resdifdir
568. mptpreima
569. mptiniseg
570. dmmpt
571. dmmptss
572. dmmptg
573. rnmpt0f
574. rnmptn0
575. dfco2
576. dfco2a
577. coundi
578. coundir
579. cores
580. resco
581. imaco
582. rnco
583. rnco2
584. dmco
585. coeq0
586. coiun
587. cocnvcnv1
588. cocnvcnv2
589. cores2
590. co02
591. co01
592. coi1
593. coi2
594. coires1
595. coass
596. relcnvtrg
597. relcnvtr
598. relssdmrn
599. relssdmrnOLD
600. resssxp
601. cnvssrndm
602. cossxp
603. relrelss
604. unielrel
605. relfld
606. relresfld
607. relcoi2
608. relcoi1
609. unidmrn
610. relcnvfld
611. dfdm2
612. unixp
613. unixp0
614. unixpid
615. ressn
616. cnviin
617. cnvpo
618. cnvso
619. xpco
620. xpcoid
621. elsnxp
622. reu3op
623. reuop
624. opreu2reurex
625. opreu2reu
626. dfpo2
627. csbcog
628. snres0
629. imaindm