![]() |
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 5440 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅)) | |
2 | df-br 4787 | . 2 ⊢ (𝐴◡𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ◡𝑅) | |
3 | df-br 4787 | . 2 ⊢ (𝐵𝑅𝐴 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) | |
4 | 1, 2, 3 | 3bitr4g 303 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∈ wcel 2145 〈cop 4322 class class class wbr 4786 ◡ccnv 5248 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pr 5034 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-br 4787 df-opab 4847 df-cnv 5257 |
This theorem is referenced by: brcnv 5443 brelrng 5493 eliniseg 5635 relbrcnvg 5645 brcodir 5656 elpredg 5837 predep 5849 dffv2 6413 ersym 7908 brdifun 7925 eqinf 8546 inflb 8551 infglb 8552 infglbb 8553 infltoreq 8564 infempty 8568 brcnvtrclfv 13952 oduleg 17340 posglbd 17358 znleval 20118 brbtwn 26000 fcoinvbr 29757 cnvordtrestixx 30299 xrge0iifiso 30321 orvcgteel 30869 inffzOLD 31953 fv1stcnv 32016 fv2ndcnv 32017 wsuclem 32107 wsuclb 32110 slenlt 32214 colineardim1 32505 gtinfOLD 32651 eldmcnv 34455 ineccnvmo 34464 alrmomorn 34465 brxrn 34478 dfcoss3 34514 brcoss3 34530 brcosscnv 34564 cosscnvssid3 34568 cosscnvssid4 34569 brnonrel 38421 ntrneifv2 38904 gte-lte 42996 gt-lt 42997 |
Copyright terms: Public domain | W3C validator |