| 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 5693 | . 2 ⊢ ◡𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑦𝑅𝑥} | |
| 4 | 1, 2, 3 | brabg 5544 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2108 class class class wbr 5143 ◡ccnv 5684 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-cnv 5693 |
| This theorem is referenced by: opelcnvg 5891 brcnv 5893 brelrng 5952 elinisegg 6111 relbrcnvg 6123 brcodir 6139 predep 6351 dffv2 7004 ersym 8757 brdifun 8775 eqinf 9524 inflb 9529 infglb 9530 infglbb 9531 infltoreq 9542 infempty 9547 brcnvtrclfv 15042 oduleg 18335 posglbdg 18460 znleval 21573 slenlt 27797 brbtwn 28914 fcoinvbr 32618 cnvordtrestixx 33912 xrge0iifiso 33934 orvcgteel 34470 fv1stcnv 35777 fv2ndcnv 35778 wsuclem 35826 wsuclb 35829 colineardim1 36062 eldmcnv 38346 ineccnvmo 38358 alrmomorn 38359 brcnvin 38371 brxrn 38375 dfcoss3 38415 cosscnv 38417 brcoss3 38434 brcosscnv 38473 cosscnvssid3 38477 cosscnvssid4 38478 brnonrel 43602 ntrneifv2 44093 glbprlem 48862 gte-lte 49243 gt-lt 49244 |
| Copyright terms: Public domain | W3C validator |