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

Theorem brcnv 5184
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 5182 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 672 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1767   _Vcvv 3113   class class class wbr 4447   `'ccnv 4998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-cnv 5007
This theorem is referenced by:  cnvco  5187  dfrn2  5190  dfdm4  5194  cnvsym  5380  intasym  5381  asymref  5382  qfto  5387  dminss  5419  imainss  5420  dminxp  5446  cnvcnv3  5455  cnvpo  5544  cnvso  5545  dffun2  5597  funcnvsn  5632  funcnv2  5646  fun2cnv  5649  imadif  5662  f1ompt  6042  foeqcnvco  6190  f1eqcocnv  6191  fliftcnv  6196  isocnv2  6214  fsplit  6888  ercnv  7332  ecid  7376  omxpenlem  7618  sbthcl  7639  fimax2g  7765  dfsup2  7901  dfsup2OLD  7902  wofib  7969  oemapso  8100  cflim2  8642  fin23lem40  8730  isfin1-3  8765  fin12  8792  negiso  10518  dfinfmr  10519  infmsup  10520  infmrgelb  10522  infmrlb  10523  xrinfmss2  11501  xrinfm0  11527  ramcl2lem  14385  imasleval  14795  invsym2  15017  oppcsect2  15029  odupos  15621  oduposb  15622  oduglb  15625  odulub  15627  posglbd  15636  gsumcom3  18684  ordtbas2  19474  ordtcnv  19484  ordtrest2  19487  utop2nei  20504  utop3cls  20505  dvlt0  22157  dvcnvrelem1  22169  ofpreima  27195  funcnvmptOLD  27197  funcnvmpt  27198  xrge0infss  27264  oduprs  27322  odutos  27329  ordtcnvNEW  27554  ordtrest2NEW  27557  xrge0iifiso  27569  ballotlemfrcn0  28124  erdszelem9  28299  coepr  28774  dffr5  28775  dfso2  28776  cnvco1  28782  cnvco2  28783  pocnv  28786  socnv  28787  wzel  28973  wsuclem  28974  txpss3v  29121  brtxp  29123  brpprod3b  29130  idsset  29133  fixcnv  29151  brimage  29169  brcup  29182  brcap  29183  dfrdg4  29193  tfrqfree  29194  dfint3  29195  imagesset  29196  brlb  29198  fvline  29387  ellines  29395  trer  29727  gtinf  29730  frinfm  29845  rencldnfilem  30374  lcmgcdlem  30828  infrglb  31156  gte-lteh  32210  gt-lth  32211  trclubg  36804
  Copyright terms: Public domain W3C validator