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 5303 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | |
4 | 1, 2, 3 | mp2an 708 | 1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∈ wcel 1990 Vcvv 3200 class class class wbr 4653 ◡ccnv 5113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-cnv 5122 |
This theorem is referenced by: cnvco 5308 dfrn2 5311 dfdm4 5316 cnvsym 5510 intasym 5511 asymref 5512 qfto 5517 dminss 5547 imainss 5548 dminxp 5574 cnvcnv3 5582 cnvpo 5673 cnvso 5674 dffun2 5898 funcnvsn 5936 funcnv2 5957 fun2cnv 5960 imadif 5973 f1ompt 6382 foeqcnvco 6555 f1eqcocnv 6556 fliftcnv 6561 isocnv2 6581 fsplit 7282 ercnv 7763 ecid 7812 omxpenlem 8061 sbthcl 8082 fimax2g 8206 dfsup2 8350 eqinf 8390 infval 8392 infcllem 8393 wofib 8450 oemapso 8579 cflim2 9085 fin23lem40 9173 isfin1-3 9208 fin12 9235 negiso 11003 dfinfre 11004 infrenegsup 11006 xrinfmss2 12141 trclublem 13734 imasleval 16201 invsym2 16423 oppcsect2 16439 odupos 17135 oduposb 17136 oduglb 17139 odulub 17141 posglbd 17150 gsumcom3 20205 ordtbas2 20995 ordtcnv 21005 ordtrest2 21008 utop2nei 22054 utop3cls 22055 dvlt0 23768 dvcnvrelem1 23780 ofpreima 29465 funcnvmptOLD 29467 funcnvmpt 29468 oduprs 29656 odutos 29663 tosglblem 29669 ordtcnvNEW 29966 ordtrest2NEW 29969 xrge0iifiso 29981 erdszelem9 31181 coepr 31642 dffr5 31643 dfso2 31644 cnvco1 31649 cnvco2 31650 pocnv 31653 wzelOLD 31772 wsuclemOLD 31774 nomaxmo 31847 txpss3v 31985 brtxp 31987 brpprod3b 31994 idsset 31997 fixcnv 32015 brimage 32033 brcup 32046 brcap 32047 dfrecs2 32057 dfrdg4 32058 dfint3 32059 imagesset 32060 brlb 32062 fvline 32251 ellines 32259 trer 32310 gtinfOLD 32314 poimirlem31 33440 poimir 33442 frinfm 33530 xrnss3v 34135 rencldnfilem 37384 cnvssco 37912 psshepw 38082 dffrege115 38272 frege131 38288 frege133 38290 gte-lteh 42467 gt-lth 42468 |
Copyright terms: Public domain | W3C validator |