![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brcnv | Structured version Visualization version GIF version |
Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
opelcnv.1 | ⊢ 𝐴 ∈ V |
opelcnv.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
brcnv | ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelcnv.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | opelcnv.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | brcnvg 5549 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | |
4 | 1, 2, 3 | mp2an 682 | 1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∈ wcel 2107 Vcvv 3398 class class class wbr 4888 ◡ccnv 5356 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pr 5140 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4889 df-opab 4951 df-cnv 5365 |
This theorem is referenced by: cnvco 5555 dfrn2 5558 dfdm4 5563 cnvsym 5767 intasym 5768 asymref 5769 qfto 5774 dminss 5803 imainss 5804 dminxp 5830 cnvcnv3 5838 cnvpo 5929 cnvso 5930 dffun2 6147 funcnvsn 6186 funcnv2 6204 fun2cnv 6207 imadif 6220 f1ompt 6647 foeqcnvco 6829 f1eqcocnv 6830 fliftcnv 6835 isocnv2 6855 fsplit 7565 ercnv 8049 ecid 8097 omxpenlem 8351 sbthcl 8372 fimax2g 8496 dfsup2 8640 eqinf 8680 infval 8682 infcllem 8683 wofib 8741 oemapso 8878 cflim2 9422 fin23lem40 9510 isfin1-3 9545 fin12 9572 negiso 11361 dfinfre 11362 infrenegsup 11364 xrinfmss2 12457 trclublem 14147 imasleval 16591 invsym2 16812 oppcsect2 16828 odupos 17525 oduposb 17526 oduglb 17529 odulub 17531 posglbd 17540 gsumcom3 20613 ordtbas2 21407 ordtcnv 21417 ordtrest2 21420 utop2nei 22466 utop3cls 22467 dvlt0 24209 dvcnvrelem1 24221 ofpreima 30034 funcnvmpt 30036 oduprs 30222 odutos 30229 tosglblem 30235 ordtcnvNEW 30568 ordtrest2NEW 30571 xrge0iifiso 30583 erdszelem9 31784 coepr 32240 dffr5 32241 dfso2 32242 cnvco1 32247 cnvco2 32248 pocnv 32251 nomaxmo 32440 txpss3v 32578 brtxp 32580 brpprod3b 32587 idsset 32590 fixcnv 32608 brimage 32626 brcup 32639 brcap 32640 dfrecs2 32650 dfrdg4 32651 dfint3 32652 imagesset 32653 brlb 32655 fvline 32844 ellines 32852 trer 32903 poimirlem31 34071 poimir 34073 frinfm 34160 xrnss3v 34767 rencldnfilem 38354 cnvssco 38879 psshepw 39048 dffrege115 39238 frege131 39254 frege133 39256 gte-lteh 43585 gt-lth 43586 |
Copyright terms: Public domain | W3C validator |