![]() |
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 5151 | . 2 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
2 | 1 | relopabi 5278 | 1 ⊢ Rel ◡𝐴 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4685 ◡ccnv 5142 Rel wrel 5148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-opab 4746 df-xp 5149 df-rel 5150 df-cnv 5151 |
This theorem is referenced by: relbrcnvg 5539 eliniseg2 5540 cnvsym 5545 intasym 5546 asymref 5547 cnvopab 5568 cnv0OLD 5571 cnvdif 5574 dfrel2 5618 cnvcnv 5621 cnvcnvOLD 5622 cnvsn0 5638 cnvcnvsn 5648 resdm2 5662 coi2 5690 coires1 5691 cnvssrndm 5695 unidmrn 5703 cnviin 5710 predep 5744 funi 5958 funcnvsn 5974 funcnv2 5995 fcnvres 6120 f1cnvcnv 6147 f1ompt 6422 fliftcnv 6601 cnvexg 7154 cnvf1o 7321 fsplit 7327 reldmtpos 7405 dmtpos 7409 rntpos 7410 dftpos3 7415 dftpos4 7416 tpostpos 7417 tposf12 7422 ercnv 7808 cnvct 8074 omxpenlem 8102 domss2 8160 cnvfi 8289 trclublem 13780 relexpaddg 13837 fsumcnv 14548 fsumcom2 14549 fsumcom2OLD 14550 fprodcnv 14757 fprodcom2 14758 fprodcom2OLD 14759 invsym2 16470 oppcsect2 16486 cnvps 17259 tsrdir 17285 mvdco 17911 gsumcom2 18420 funcnvmptOLD 29595 funcnvmpt 29596 fcnvgreu 29600 dfcnv2 29604 gsummpt2co 29908 cnvco1 31775 cnvco2 31776 colinrel 32289 trer 32435 releleccnv 34162 eleccnvep 34187 cnvresrn 34256 ineccnvmo 34262 elec1cnvxrn2 34295 cnvelrels 34385 cnvnonrel 38211 cnvcnvintabd 38223 cnvintabd 38226 cnvssco 38229 clrellem 38246 clcnvlem 38247 cnviun 38259 trrelsuperrel2dg 38280 dffrege115 38589 |
Copyright terms: Public domain | W3C validator |