![]() |
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 5152 | . 2 ⊢ (𝑥 = 𝐴 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐴)) | |
2 | breq1 5151 | . 2 ⊢ (𝑦 = 𝐵 → (𝑦𝑅𝐴 ↔ 𝐵𝑅𝐴)) | |
3 | df-cnv 5697 | . 2 ⊢ ◡𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑦𝑅𝑥} | |
4 | 1, 2, 3 | brabg 5549 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2106 class class class wbr 5148 ◡ccnv 5688 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-br 5149 df-opab 5211 df-cnv 5697 |
This theorem is referenced by: opelcnvg 5894 brcnv 5896 brelrng 5955 elinisegg 6114 relbrcnvg 6126 brcodir 6142 predep 6353 dffv2 7004 ersym 8756 brdifun 8774 eqinf 9522 inflb 9527 infglb 9528 infglbb 9529 infltoreq 9540 infempty 9545 brcnvtrclfv 15039 oduleg 18347 posglbdg 18473 znleval 21591 slenlt 27812 brbtwn 28929 fcoinvbr 32625 cnvordtrestixx 33874 xrge0iifiso 33896 orvcgteel 34449 fv1stcnv 35758 fv2ndcnv 35759 wsuclem 35807 wsuclb 35810 colineardim1 36043 eldmcnv 38327 ineccnvmo 38339 alrmomorn 38340 brcnvin 38352 brxrn 38356 dfcoss3 38396 cosscnv 38398 brcoss3 38415 brcosscnv 38454 cosscnvssid3 38458 cosscnvssid4 38459 brnonrel 43579 ntrneifv2 44070 glbprlem 48762 gte-lte 48955 gt-lt 48956 |
Copyright terms: Public domain | W3C validator |