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

Theorem brcnv 4817
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 4815 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 656 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1621   _Vcvv 2740   class class class wbr 3963   `'ccnv 4625
This theorem is referenced by:  cnvco  4818  dfrn2  4821  dfdm4  4825  cnvsym  5010  intasym  5011  asymref  5012  qfto  5017  dminss  5048  imainss  5049  dminxp  5071  cnvcnv3  5076  cnvpo  5165  cnvso  5166  dffun2  5169  funcnvsn  5200  funcnv2  5212  fun2cnv  5215  imadif  5230  f1ompt  5581  foeqcnvco  5703  f1eqcocnv  5704  fliftcnv  5709  isocnv2  5727  fsplit  6122  ercnv  6614  ecid  6657  omxpenlem  6896  sbthcl  6916  fimax2g  7036  dfsup2  7128  dfsup2OLD  7129  wofib  7193  oemapso  7317  cflim2  7822  fin23lem40  7910  isfin1-3  7945  fin12  7972  negiso  9663  dfinfmr  9664  infmsup  9665  infmrgelb  9667  infmrlb  9668  xrinfmss2  10560  xrinfm0  10586  ramcl2lem  12983  imasleval  13370  invsym2  13592  oppcsect2  13604  odupos  14166  oduposb  14167  oduglb  14170  odulub  14172  posglbd  14180  ordtbas2  16848  ordtcnv  16858  ordtrest2  16861  dvlt0  19279  dvcnvrelem1  19291  ballotlemfrcn0  23014  erdszelem9  23067  coepr  23445  dffr5  23446  dfso2  23447  cnvco1  23453  cnvco2  23454  txpss3v  23759  brtxp  23761  brpprod3b  23768  idsset  23771  fixcnv  23789  brimage  23805  brcup  23818  brcap  23819  dfrdg4  23828  tfrqfree  23829  fvline  24107  ellines  24115  defse3  24604  trer  25559  gtinf  25566  frinfm  25748  rencldnfilem  26235  gsumcom3  26786  gte-lteh  27208  gt-lth  27209
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-br 3964  df-opab 4018  df-cnv 4642
  Copyright terms: Public domain W3C validator