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 5046 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
2 | 1 | relopabi 5167 | 1 ⊢ Rel ◡𝐴 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4583 ◡ccnv 5037 Rel wrel 5043 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-opab 4644 df-xp 5044 df-rel 5045 df-cnv 5046 |
This theorem is referenced by: relbrcnvg 5423 eliniseg2 5424 cnvsym 5429 intasym 5430 asymref 5431 cnvopab 5452 cnv0OLD 5455 cnvdif 5458 dfrel2 5502 cnvcnv 5505 cnvsn0 5521 cnvcnvsn 5530 resdm2 5542 coi2 5569 coires1 5570 cnvssrndm 5574 unidmrn 5582 cnviin 5589 predep 5623 funi 5834 funcnvsn 5850 funcnv2 5871 fcnvres 5995 f1cnvcnv 6022 f1ompt 6290 fliftcnv 6461 cnvexg 7005 cnvf1o 7163 fsplit 7169 reldmtpos 7247 dmtpos 7251 rntpos 7252 dftpos3 7257 dftpos4 7258 tpostpos 7259 tposf12 7264 ercnv 7650 omxpenlem 7946 domss2 8004 cnvfi 8131 trclublem 13582 relexpaddg 13641 fsumcnv 14346 fsumcom2 14347 fsumcom2OLD 14348 fprodcnv 14552 fprodcom2 14553 fprodcom2OLD 14554 invsym2 16246 oppcsect2 16262 cnvps 17035 tsrdir 17061 mvdco 17688 gsumcom2 18197 funcnvmptOLD 28850 funcnvmpt 28851 fcnvgreu 28855 dfcnv2 28859 cnvct 28878 gsummpt2co 29111 cnvco1 30903 cnvco2 30904 colinrel 31334 trer 31480 cnvnonrel 36913 cnvcnvintabd 36925 cnvintabd 36928 cnvssco 36931 clrellem 36948 clcnvlem 36949 cnviun 36961 trrelsuperrel2dg 36982 dffrege115 37292 |
Copyright terms: Public domain | W3C validator |