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 | breq2 5083 | . 2 ⊢ (𝑥 = 𝐴 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐴)) | |
2 | breq1 5082 | . 2 ⊢ (𝑦 = 𝐵 → (𝑦𝑅𝐴 ↔ 𝐵𝑅𝐴)) | |
3 | df-cnv 5598 | . 2 ⊢ ◡𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑦𝑅𝑥} | |
4 | 1, 2, 3 | brabg 5455 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∈ wcel 2110 class class class wbr 5079 ◡ccnv 5589 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 ax-sep 5227 ax-nul 5234 ax-pr 5356 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-nul 4263 df-if 4466 df-sn 4568 df-pr 4570 df-op 4574 df-br 5080 df-opab 5142 df-cnv 5598 |
This theorem is referenced by: opelcnvg 5788 brcnv 5790 brelrng 5849 elinisegg 6000 relbrcnvg 6012 brcodir 6023 predep 6232 dffv2 6860 ersym 8493 brdifun 8510 eqinf 9221 inflb 9226 infglb 9227 infglbb 9228 infltoreq 9239 infempty 9244 brcnvtrclfv 14712 oduleg 18006 posglbdg 18131 znleval 20760 brbtwn 27265 fcoinvbr 30943 cnvordtrestixx 31859 xrge0iifiso 31881 orvcgteel 32430 fv1stcnv 33747 fv2ndcnv 33748 wsuclem 33815 wsuclb 33818 slenlt 33951 colineardim1 34359 eldmcnv 36476 ineccnvmo 36485 alrmomorn 36486 brxrn 36500 dfcoss3 36536 brcoss3 36552 brcosscnv 36586 cosscnvssid3 36590 cosscnvssid4 36591 brnonrel 41167 ntrneifv2 41660 glbprlem 46228 gte-lte 46395 gt-lt 46396 |
Copyright terms: Public domain | W3C validator |