Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > brcnv | Structured version Visualization version GIF version |
Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
opelcnv.1 | ⊢ 𝐴 ∈ V |
opelcnv.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
brcnv | ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelcnv.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | opelcnv.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | brcnvg 5743 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∈ wcel 2105 Vcvv 3492 class class class wbr 5057 ◡ccnv 5547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-cnv 5556 |
This theorem is referenced by: cnvco 5749 dfrn2 5752 dfdm4 5757 cnvsym 5967 intasym 5968 asymref 5969 qfto 5974 dminss 6003 imainss 6004 dminxp 6030 cnvcnv3 6038 cnvpo 6131 cnvso 6132 dffun2 6358 funcnvsn 6397 funcnv2 6415 fun2cnv 6418 imadif 6431 f1ompt 6867 foeqcnvco 7047 f1eqcocnv 7048 fliftcnv 7053 isocnv2 7073 fsplit 7801 fsplitOLD 7802 ercnv 8299 ecid 8351 omxpenlem 8606 sbthcl 8627 fimax2g 8752 dfsup2 8896 eqinf 8936 infval 8938 infcllem 8939 wofib 8997 oemapso 9133 cflim2 9673 fin23lem40 9761 isfin1-3 9796 fin12 9823 negiso 11609 dfinfre 11610 infrenegsup 11612 xrinfmss2 12692 trclublem 14343 imasleval 16802 invsym2 17021 oppcsect2 17037 odupos 17733 oduposb 17734 oduglb 17737 odulub 17739 posglbd 17748 gsumcom3 19027 ordtbas2 21727 ordtcnv 21737 ordtrest2 21740 utop2nei 22786 utop3cls 22787 dvlt0 24529 dvcnvrelem1 24541 ofpreima 30338 funcnvmpt 30340 oduprs 30570 odutos 30577 tosglblem 30583 ordtcnvNEW 31062 ordtrest2NEW 31065 xrge0iifiso 31077 erdszelem9 32343 coepr 32885 dffr5 32886 dfso2 32887 cnvco1 32892 cnvco2 32893 pocnv 32896 nomaxmo 33098 txpss3v 33236 brtxp 33238 brpprod3b 33245 idsset 33248 fixcnv 33266 brimage 33284 brcup 33297 brcap 33298 dfrecs2 33308 dfrdg4 33309 dfint3 33310 imagesset 33311 brlb 33313 fvline 33502 ellines 33510 trer 33561 poimirlem31 34804 poimir 34806 frinfm 34891 xrnss3v 35504 rencldnfilem 39295 cnvssco 39844 psshepw 40012 dffrege115 40202 frege131 40218 frege133 40220 gte-lteh 44753 gt-lth 44754 |
Copyright terms: Public domain | W3C validator |