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

Theorem brcnv 4995
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 4993 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 654 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1717   _Vcvv 2899   class class class wbr 4153   `'ccnv 4817
This theorem is referenced by:  cnvco  4996  dfrn2  4999  dfdm4  5003  cnvsym  5188  intasym  5189  asymref  5190  qfto  5195  dminss  5226  imainss  5227  dminxp  5251  cnvcnv3  5260  cnvpo  5350  cnvso  5351  dffun2  5404  funcnvsn  5436  funcnv2  5450  fun2cnv  5453  imadif  5468  f1ompt  5830  foeqcnvco  5966  f1eqcocnv  5967  fliftcnv  5972  isocnv2  5990  fsplit  6390  ercnv  6862  ecid  6905  omxpenlem  7145  sbthcl  7165  fimax2g  7289  dfsup2  7382  dfsup2OLD  7383  wofib  7447  oemapso  7571  cflim2  8076  fin23lem40  8164  isfin1-3  8199  fin12  8226  negiso  9916  dfinfmr  9917  infmsup  9918  infmrgelb  9920  infmrlb  9921  xrinfmss2  10821  xrinfm0  10847  ramcl2lem  13304  imasleval  13693  invsym2  13915  oppcsect2  13927  odupos  14489  oduposb  14490  oduglb  14493  odulub  14495  posglbd  14503  ordtbas2  17177  ordtcnv  17187  ordtrest2  17190  utop2nei  18201  utop3cls  18202  dvlt0  19756  dvcnvrelem1  19768  funcnvmptOLD  23923  funcnvmpt  23924  xrge0iifiso  24125  ballotlemfrcn0  24566  erdszelem9  24664  coepr  25133  dffr5  25134  dfso2  25135  cnvco1  25141  cnvco2  25142  txpss3v  25442  brtxp  25444  brpprod3b  25451  idsset  25454  fixcnv  25472  brimage  25489  brcup  25502  brcap  25503  dfrdg4  25513  tfrqfree  25514  fvline  25792  ellines  25800  trer  26010  gtinf  26013  frinfm  26128  rencldnfilem  26572  gsumcom3  27123  infrglb  27390  gte-lteh  27815  gt-lth  27816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-cnv 4826
  Copyright terms: Public domain W3C validator