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 5225 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | |
4 | 1, 2, 3 | mp2an 704 | 1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∈ wcel 1977 Vcvv 3173 class class class wbr 4583 ◡ccnv 5037 |
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-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
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-eu 2462 df-mo 2463 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-br 4584 df-opab 4644 df-cnv 5046 |
This theorem is referenced by: cnvco 5230 dfrn2 5233 dfdm4 5238 cnvsym 5429 intasym 5430 asymref 5431 qfto 5436 dminss 5466 imainss 5467 dminxp 5493 cnvcnv3 5501 cnvpo 5590 cnvso 5591 dffun2 5814 funcnvsn 5850 funcnv2 5871 fun2cnv 5874 imadif 5887 f1ompt 6290 foeqcnvco 6455 f1eqcocnv 6456 fliftcnv 6461 isocnv2 6481 fsplit 7169 ercnv 7650 ecid 7699 omxpenlem 7946 sbthcl 7967 fimax2g 8091 dfsup2 8233 eqinf 8273 infval 8275 infcllem 8276 wofib 8333 oemapso 8462 cflim2 8968 fin23lem40 9056 isfin1-3 9091 fin12 9118 negiso 10880 dfinfre 10881 infrenegsup 10883 xrinfmss2 12013 trclublem 13582 imasleval 16024 invsym2 16246 oppcsect2 16262 odupos 16958 oduposb 16959 oduglb 16962 odulub 16964 posglbd 16973 gsumcom3 20024 ordtbas2 20805 ordtcnv 20815 ordtrest2 20818 utop2nei 21864 utop3cls 21865 dvlt0 23572 dvcnvrelem1 23584 ofpreima 28848 funcnvmptOLD 28850 funcnvmpt 28851 oduprs 28987 odutos 28994 tosglblem 29000 ordtcnvNEW 29294 ordtrest2NEW 29297 xrge0iifiso 29309 erdszelem9 30435 coepr 30895 dffr5 30896 dfso2 30897 cnvco1 30903 cnvco2 30904 pocnv 30907 socnv 30908 wzelOLD 31016 wsuclemOLD 31018 txpss3v 31155 brtxp 31157 brpprod3b 31164 idsset 31167 fixcnv 31185 brimage 31203 brcup 31216 brcap 31217 dfrecs2 31227 dfrdg4 31228 dfint3 31229 imagesset 31230 brlb 31232 fvline 31421 ellines 31429 trer 31480 gtinfOLD 31484 poimirlem31 32610 poimir 32612 frinfm 32700 rencldnfilem 36402 cnvssco 36931 psshepw 37102 dffrege115 37292 frege131 37308 frege133 37310 gte-lteh 42266 gt-lth 42267 |
Copyright terms: Public domain | W3C validator |