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

Theorem brcnv 4863
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  |-  A  e. 
_V
opelcnv.2  |-  B  e. 
_V
Assertion
Ref Expression
brcnv  |-  ( A `' R B  <->  B R A )

Proof of Theorem brcnv
StepHypRef Expression
1 opelcnv.1 . 2  |-  A  e. 
_V
2 opelcnv.2 . 2  |-  B  e. 
_V
3 brcnvg 4861 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 653 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1685   _Vcvv 2789   class class class wbr 4024   `'ccnv 4687
This theorem is referenced by:  cnvco  4864  dfrn2  4867  dfdm4  4871  cnvsym  5056  intasym  5057  asymref  5058  qfto  5063  dminss  5094  imainss  5095  dminxp  5117  cnvcnv3  5122  cnvpo  5211  cnvso  5212  dffun2  5231  funcnvsn  5263  funcnv2  5275  fun2cnv  5278  imadif  5293  f1ompt  5644  foeqcnvco  5766  f1eqcocnv  5767  fliftcnv  5772  isocnv2  5790  fsplit  6185  ercnv  6677  ecid  6720  omxpenlem  6959  sbthcl  6979  fimax2g  7099  dfsup2  7191  dfsup2OLD  7192  wofib  7256  oemapso  7380  cflim2  7885  fin23lem40  7973  isfin1-3  8008  fin12  8035  negiso  9726  dfinfmr  9727  infmsup  9728  infmrgelb  9730  infmrlb  9731  xrinfmss2  10625  xrinfm0  10651  ramcl2lem  13052  imasleval  13439  invsym2  13661  oppcsect2  13673  odupos  14235  oduposb  14236  oduglb  14239  odulub  14241  posglbd  14249  ordtbas2  16917  ordtcnv  16927  ordtrest2  16930  dvlt0  19348  dvcnvrelem1  19360  ballotlemfrcn0  23084  erdszelem9  23137  coepr  23515  dffr5  23516  dfso2  23517  cnvco1  23523  cnvco2  23524  txpss3v  23829  brtxp  23831  brpprod3b  23838  idsset  23841  fixcnv  23859  brimage  23875  brcup  23888  brcap  23889  dfrdg4  23898  tfrqfree  23899  fvline  24177  ellines  24185  defse3  24683  trer  25638  gtinf  25645  frinfm  25827  rencldnfilem  26314  gsumcom3  26865  infrglb  27133  gte-lteh  27468  gt-lth  27469
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-cnv 4696
  Copyright terms: Public domain W3C validator