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

Theorem brcnv 4852
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 4850 . 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 2763   class class class wbr 3997   `'ccnv 4660
This theorem is referenced by:  cnvco  4853  dfrn2  4856  dfdm4  4860  cnvsym  5045  intasym  5046  asymref  5047  qfto  5052  dminss  5083  imainss  5084  dminxp  5106  cnvcnv3  5111  cnvpo  5200  cnvso  5201  dffun2  5204  funcnvsn  5235  funcnv2  5247  fun2cnv  5250  imadif  5265  f1ompt  5616  foeqcnvco  5738  f1eqcocnv  5739  fliftcnv  5744  isocnv2  5762  fsplit  6157  ercnv  6649  ecid  6692  omxpenlem  6931  sbthcl  6951  fimax2g  7071  dfsup2  7163  dfsup2OLD  7164  wofib  7228  oemapso  7352  cflim2  7857  fin23lem40  7945  isfin1-3  7980  fin12  8007  negiso  9698  dfinfmr  9699  infmsup  9700  infmrgelb  9702  infmrlb  9703  xrinfmss2  10596  xrinfm0  10622  ramcl2lem  13019  imasleval  13406  invsym2  13628  oppcsect2  13640  odupos  14202  oduposb  14203  oduglb  14206  odulub  14208  posglbd  14216  ordtbas2  16884  ordtcnv  16894  ordtrest2  16897  dvlt0  19315  dvcnvrelem1  19327  ballotlemfrcn0  23050  erdszelem9  23103  coepr  23481  dffr5  23482  dfso2  23483  cnvco1  23489  cnvco2  23490  txpss3v  23795  brtxp  23797  brpprod3b  23804  idsset  23807  fixcnv  23825  brimage  23841  brcup  23854  brcap  23855  dfrdg4  23864  tfrqfree  23865  fvline  24143  ellines  24151  defse3  24640  trer  25595  gtinf  25602  frinfm  25784  rencldnfilem  26271  gsumcom3  26822  infrglb  27091  gte-lteh  27329  gt-lth  27330
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 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
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 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-br 3998  df-opab 4052  df-cnv 4677
  Copyright terms: Public domain W3C validator