![]() |
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 5886 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2099 Vcvv 3462 class class class wbr 5153 ◡ccnv 5681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-br 5154 df-opab 5216 df-cnv 5690 |
This theorem is referenced by: cnvco 5892 dfrn2 5895 dfdm4 5902 cnvsym 6124 cnvsymOLD 6125 cnvsymOLDOLD 6126 intasym 6127 asymref 6128 qfto 6133 dminss 6164 imainss 6165 dminxp 6191 cnvcnv3 6199 cnvpo 6298 cnvso 6299 dffun2 6564 dffun2OLD 6565 dffun2OLDOLD 6566 funcnvsn 6609 funcnv2 6627 fun2cnv 6630 imadif 6643 f1ompt 7125 foeqcnvco 7314 f1eqcocnv 7315 fliftcnv 7323 isocnv2 7343 fsplit 8131 ercnv 8755 ecid 8811 omxpenlem 9111 sbthcl 9133 fimax2g 9323 dfsup2 9487 eqinf 9527 infval 9529 infcllem 9530 wofib 9588 oemapso 9725 cflim2 10306 fin23lem40 10394 isfin1-3 10429 fin12 10456 negiso 12246 dfinfre 12247 infrenegsup 12249 xrinfmss2 13344 trclublem 15000 imasleval 17556 invsym2 17779 oppcsect2 17795 odupos 18353 oduposb 18354 odulub 18432 oduglb 18434 posglbdg 18440 gsumcom3 19976 ordtbas2 23186 ordtcnv 23196 ordtrest2 23199 utop2nei 24246 utop3cls 24247 dvlt0 26029 dvcnvrelem1 26041 nomaxmo 27728 ofpreima 32582 funcnvmpt 32584 oduprs 32834 odutos 32838 tosglblem 32844 mgccnv 32869 ordtcnvNEW 33735 ordtrest2NEW 33738 xrge0iifiso 33750 erdszelem9 35027 coepr 35575 dffr5 35576 dfso2 35577 cnvco1 35581 cnvco2 35582 pocnv 35585 txpss3v 35702 brtxp 35704 brpprod3b 35711 idsset 35714 fixcnv 35732 brimage 35750 brcup 35763 brcap 35764 dfrecs2 35774 dfrdg4 35775 dfint3 35776 imagesset 35777 brlb 35779 fvline 35968 ellines 35976 trer 36028 poimirlem31 37352 poimir 37354 frinfm 37436 xrnss3v 38070 rencldnfilem 42477 cnvssco 43273 psshepw 43455 dffrege115 43645 frege131 43661 frege133 43663 gte-lteh 48472 gt-lth 48473 |
Copyright terms: Public domain | W3C validator |