![]() |
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 5147 | . 2 ⊢ (𝑥 = 𝐴 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐴)) | |
2 | breq1 5146 | . 2 ⊢ (𝑦 = 𝐵 → (𝑦𝑅𝐴 ↔ 𝐵𝑅𝐴)) | |
3 | df-cnv 5681 | . 2 ⊢ ◡𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑦𝑅𝑥} | |
4 | 1, 2, 3 | brabg 5536 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∈ wcel 2099 class class class wbr 5143 ◡ccnv 5672 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5294 ax-nul 5301 ax-pr 5424 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3429 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4526 df-sn 4626 df-pr 4628 df-op 4632 df-br 5144 df-opab 5206 df-cnv 5681 |
This theorem is referenced by: opelcnvg 5878 brcnv 5880 brelrng 5938 elinisegg 6092 relbrcnvg 6104 brcodir 6120 predep 6331 dffv2 6988 ersym 8731 brdifun 8748 eqinf 9502 inflb 9507 infglb 9508 infglbb 9509 infltoreq 9520 infempty 9525 brcnvtrclfv 14977 oduleg 18276 posglbdg 18401 znleval 21482 slenlt 27679 brbtwn 28704 fcoinvbr 32389 cnvordtrestixx 33509 xrge0iifiso 33531 orvcgteel 34082 fv1stcnv 35367 fv2ndcnv 35368 wsuclem 35416 wsuclb 35419 colineardim1 35652 eldmcnv 37812 ineccnvmo 37824 alrmomorn 37825 brcnvin 37837 brxrn 37841 dfcoss3 37881 cosscnv 37883 brcoss3 37900 brcosscnv 37939 cosscnvssid3 37943 cosscnvssid4 37944 brnonrel 43010 ntrneifv2 43501 glbprlem 47975 gte-lte 48146 gt-lt 48147 |
Copyright terms: Public domain | W3C validator |