MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brcnv Structured version   Visualization version   GIF version

Theorem brcnv 5734
Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
Hypotheses
Ref Expression
opelcnv.1 𝐴 ∈ V
opelcnv.2 𝐵 ∈ V
Assertion
Ref Expression
brcnv (𝐴𝑅𝐵𝐵𝑅𝐴)

Proof of Theorem brcnv
StepHypRef Expression
1 opelcnv.1 . 2 𝐴 ∈ V
2 opelcnv.2 . 2 𝐵 ∈ V
3 brcnvg 5731 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 691 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wcel 2115  Vcvv 3479   class class class wbr 5047  ccnv 5535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pr 5311
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-br 5048  df-opab 5110  df-cnv 5544
This theorem is referenced by:  cnvco  5737  dfrn2  5740  dfdm4  5745  cnvsym  5955  intasym  5956  asymref  5957  qfto  5962  dminss  5991  imainss  5992  dminxp  6018  cnvcnv3  6026  cnvpo  6119  cnvso  6120  dffun2  6346  funcnvsn  6385  funcnv2  6403  fun2cnv  6406  imadif  6419  f1ompt  6856  foeqcnvco  7038  f1eqcocnv  7039  fliftcnv  7046  isocnv2  7066  fsplit  7795  fsplitOLD  7796  ercnv  8293  ecid  8345  omxpenlem  8601  sbthcl  8623  fimax2g  8748  dfsup2  8892  eqinf  8932  infval  8934  infcllem  8935  wofib  8993  oemapso  9129  cflim2  9670  fin23lem40  9758  isfin1-3  9793  fin12  9820  negiso  11606  dfinfre  11607  infrenegsup  11609  xrinfmss2  12690  trclublem  14344  imasleval  16803  invsym2  17022  oppcsect2  17038  odupos  17734  oduposb  17735  oduglb  17738  odulub  17740  posglbd  17749  gsumcom3  19087  ordtbas2  21785  ordtcnv  21795  ordtrest2  21798  utop2nei  22845  utop3cls  22846  dvlt0  24597  dvcnvrelem1  24609  ofpreima  30407  funcnvmpt  30409  oduprs  30640  odutos  30647  tosglblem  30653  mcgcnv  30676  ordtcnvNEW  31181  ordtrest2NEW  31184  xrge0iifiso  31196  erdszelem9  32464  coepr  33006  dffr5  33007  dfso2  33008  cnvco1  33013  cnvco2  33014  pocnv  33017  nomaxmo  33219  txpss3v  33357  brtxp  33359  brpprod3b  33366  idsset  33369  fixcnv  33387  brimage  33405  brcup  33418  brcap  33419  dfrecs2  33429  dfrdg4  33430  dfint3  33431  imagesset  33432  brlb  33434  fvline  33623  ellines  33631  trer  33682  poimirlem31  34988  poimir  34990  frinfm  35073  xrnss3v  35684  rencldnfilem  39593  cnvssco  40138  psshepw  40322  dffrege115  40512  frege131  40528  frege133  40530  gte-lteh  45082  gt-lth  45083
  Copyright terms: Public domain W3C validator