| 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 5890 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∈ wcel 2108 Vcvv 3480 class class class wbr 5143 ◡ccnv 5684 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-cnv 5693 |
| This theorem is referenced by: cnvco 5896 dfrn2 5899 dfdm4 5906 cnvsym 6132 cnvsymOLD 6133 cnvsymOLDOLD 6134 intasym 6135 asymref 6136 qfto 6141 dminss 6173 imainss 6174 dminxp 6200 cnvcnv3 6208 cnvpo 6307 cnvso 6308 dffun2 6571 dffun2OLD 6572 dffun2OLDOLD 6573 funcnvsn 6616 funcnv2 6634 fun2cnv 6637 imadif 6650 f1ompt 7131 foeqcnvco 7320 f1eqcocnv 7321 fliftcnv 7331 isocnv2 7351 fsplit 8142 ercnv 8766 ecid 8822 omxpenlem 9113 sbthcl 9135 fimax2g 9322 dfsup2 9484 eqinf 9524 infval 9526 infcllem 9527 wofib 9585 oemapso 9722 cflim2 10303 fin23lem40 10391 isfin1-3 10426 fin12 10453 negiso 12248 dfinfre 12249 infrenegsup 12251 xrinfmss2 13353 trclublem 15034 imasleval 17586 invsym2 17807 oppcsect2 17823 oduprs 18346 odupos 18373 oduposb 18374 odulub 18452 oduglb 18454 posglbdg 18460 gsumcom3 19996 ordtbas2 23199 ordtcnv 23209 ordtrest2 23212 utop2nei 24259 utop3cls 24260 dvlt0 26044 dvcnvrelem1 26056 nomaxmo 27743 ofpreima 32675 funcnvmpt 32677 odutos 32958 tosglblem 32964 mgccnv 32989 ordtcnvNEW 33919 ordtrest2NEW 33922 xrge0iifiso 33934 erdszelem9 35204 coepr 35753 dffr5 35754 dfso2 35755 cnvco1 35759 cnvco2 35760 pocnv 35763 txpss3v 35879 brtxp 35881 brpprod3b 35888 idsset 35891 fixcnv 35909 brimage 35927 brcup 35940 brcap 35941 dfrecs2 35951 dfrdg4 35952 dfint3 35953 imagesset 35954 brlb 35956 fvline 36145 ellines 36153 trer 36317 poimirlem31 37658 poimir 37660 frinfm 37742 xrnss3v 38373 rencldnfilem 42831 cnvssco 43619 psshepw 43801 dffrege115 43991 frege131 44007 frege133 44009 gte-lteh 49245 gt-lth 49246 |
| Copyright terms: Public domain | W3C validator |