| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > relcnv | Structured version Visualization version GIF version | ||
| Description: A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.) |
| Ref | Expression |
|---|---|
| relcnv | ⊢ Rel ◡𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-cnv 5693 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
| 2 | 1 | relopabiv 5830 | 1 ⊢ Rel ◡𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: class class class wbr 5143 ◡ccnv 5684 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 df-cnv 5693 |
| This theorem is referenced by: relbrcnvg 6123 eliniseg2 6124 cnvsym 6132 cnvsymOLD 6133 cnvsymOLDOLD 6134 intasym 6135 asymref 6136 cnvopab 6157 cnvopabOLD 6158 cnvdif 6163 dfrel2 6209 cnvcnv 6212 cnvsn0 6230 cnvcnvsn 6239 resdm2 6251 coi2 6283 coires1 6284 cnvssrndm 6291 unidmrn 6299 cnviin 6306 predep 6351 funi 6598 funcnvsn 6616 funcnv2 6634 fcnvres 6785 f1cnvcnv 6813 f1ompt 7131 fliftcnv 7331 cnvexg 7946 cnvf1o 8136 fsplit 8142 reldmtpos 8259 dmtpos 8263 rntpos 8264 dftpos3 8269 dftpos4 8270 tpostpos 8271 tposf12 8276 ercnv 8766 cnvct 9074 omxpenlem 9113 domss2 9176 cnvfi 9216 cnvfiALT 9379 trclublem 15034 relexpaddg 15092 fsumcnv 15809 fsumcom2 15810 fprodcnv 16019 fprodcom2 16020 invsym2 17807 oppcsect2 17823 cnvps 18623 tsrdir 18649 mvdco 19463 gsumcom2 19993 funcnvmpt 32677 fcnvgreu 32683 dfcnv2 32686 gsummpt2co 33051 gsumhashmul 33064 cnvco1 35759 cnvco2 35760 colinrel 36058 trer 36317 releleccnv 38258 eleccnvep 38282 brcnvrabga 38343 cnvresrn 38349 ineccnvmo 38358 elec1cnvxrn2 38398 cnvelrels 38496 dfdisjALTV 38714 dfeldisj5 38722 dfantisymrel4 38762 dfantisymrel5 38763 cnvnonrel 43601 cnvcnvintabd 43613 cnvintabd 43616 cnvssco 43619 clrellem 43635 clcnvlem 43636 cnviun 43663 trrelsuperrel2dg 43684 dffrege115 43991 dmtposss 48776 tposrescnv 48779 tposres3 48781 tposideq 48788 |
| Copyright terms: Public domain | W3C validator |