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

Theorem brcnv 4880
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 4878 . 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 1696   _Vcvv 2801   class class class wbr 4039   `'ccnv 4704
This theorem is referenced by:  cnvco  4881  dfrn2  4884  dfdm4  4888  cnvsym  5073  intasym  5074  asymref  5075  qfto  5080  dminss  5111  imainss  5112  dminxp  5134  cnvcnv3  5139  cnvpo  5229  cnvso  5230  dffun2  5281  funcnvsn  5313  funcnv2  5325  fun2cnv  5328  imadif  5343  f1ompt  5698  foeqcnvco  5820  f1eqcocnv  5821  fliftcnv  5826  isocnv2  5844  fsplit  6239  ercnv  6697  ecid  6740  omxpenlem  6979  sbthcl  6999  fimax2g  7119  dfsup2  7211  dfsup2OLD  7212  wofib  7276  oemapso  7400  cflim2  7905  fin23lem40  7993  isfin1-3  8028  fin12  8055  negiso  9746  dfinfmr  9747  infmsup  9748  infmrgelb  9750  infmrlb  9751  xrinfmss2  10645  xrinfm0  10671  ramcl2lem  13072  imasleval  13459  invsym2  13681  oppcsect2  13693  odupos  14255  oduposb  14256  oduglb  14259  odulub  14261  posglbd  14269  ordtbas2  16937  ordtcnv  16947  ordtrest2  16950  dvlt0  19368  dvcnvrelem1  19380  ballotlemfrcn0  23104  funcnvmptOLD  23249  funcnvmpt  23250  erdszelem9  23745  coepr  24180  dffr5  24181  dfso2  24182  cnvco1  24188  cnvco2  24189  txpss3v  24489  brtxp  24491  brpprod3b  24498  idsset  24501  fixcnv  24519  brimage  24536  brcup  24549  brcap  24550  dfrdg4  24560  tfrqfree  24561  fvline  24839  ellines  24847  defse3  25375  trer  26330  gtinf  26337  frinfm  26519  rencldnfilem  27006  gsumcom3  27557  infrglb  27825  gte-lteh  28450  gt-lth  28451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-cnv 4713
  Copyright terms: Public domain W3C validator