![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brcnvg | Structured version Visualization version GIF version |
Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.) |
Ref | Expression |
---|---|
brcnvg | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelcnvg 5449 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅)) | |
2 | df-br 4797 | . 2 ⊢ (𝐴◡𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ◡𝑅) | |
3 | df-br 4797 | . 2 ⊢ (𝐵𝑅𝐴 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) | |
4 | 1, 2, 3 | 3bitr4g 303 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∈ wcel 2131 〈cop 4319 class class class wbr 4796 ◡ccnv 5257 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pr 5047 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-rab 3051 df-v 3334 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-sn 4314 df-pr 4316 df-op 4320 df-br 4797 df-opab 4857 df-cnv 5266 |
This theorem is referenced by: brcnv 5452 brelrng 5502 eliniseg 5644 relbrcnvg 5654 brcodir 5665 elpredg 5847 predep 5859 dffv2 6425 ersym 7915 brdifun 7932 eqinf 8547 inflb 8552 infglb 8553 infglbb 8554 infltoreq 8565 infempty 8569 brcnvtrclfv 13935 oduleg 17325 posglbd 17343 znleval 20097 brbtwn 25970 fcoinvbr 29718 cnvordtrestixx 30260 xrge0iifiso 30282 orvcgteel 30830 inffzOLD 31914 fv1stcnv 31977 fv2ndcnv 31978 wsuclem 32068 wsuclb 32071 slenlt 32175 colineardim1 32466 gtinfOLD 32612 eldmcnv 34428 ineccnvmo 34437 alrmomorn 34438 brxrn 34451 dfcoss3 34487 brcoss3 34503 brcosscnv 34537 cosscnvssid3 34541 cosscnvssid4 34542 brnonrel 38389 ntrneifv2 38872 gte-lte 42970 gt-lt 42971 |
Copyright terms: Public domain | W3C validator |