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

Theorem brcnv 5022
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 5020 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 686 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    e. wcel 1904   _Vcvv 3031   class class class wbr 4395   `'ccnv 4838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-cnv 4847
This theorem is referenced by:  cnvco  5025  dfrn2  5028  dfdm4  5032  cnvsym  5220  intasym  5221  asymref  5222  qfto  5227  dminss  5256  imainss  5257  dminxp  5283  cnvcnv3  5291  cnvpo  5381  cnvso  5382  dffun2  5599  funcnvsn  5634  funcnv2  5652  fun2cnv  5655  imadif  5668  f1ompt  6059  foeqcnvco  6216  f1eqcocnv  6217  fliftcnv  6222  isocnv2  6240  fsplit  6920  ercnv  7402  ecid  7446  omxpenlem  7691  sbthcl  7712  fimax2g  7835  dfsup2  7976  eqinf  8018  infval  8020  infcllem  8021  wofib  8078  oemapso  8205  cflim2  8711  fin23lem40  8799  isfin1-3  8834  fin12  8861  negiso  10609  dfinfre  10610  dfinfmrOLD  10611  infrenegsup  10613  infmsupOLD  10614  infmrgelbOLD  10617  infmrlbOLD  10619  xrinfmss2  11621  xrinfm0OLD  11652  trclublem  13134  ramcl2lemOLD  15042  imasleval  15525  invsym2  15746  oppcsect2  15762  odupos  16459  oduposb  16460  oduglb  16463  odulub  16465  posglbd  16474  gsumcom3  19501  ordtbas2  20284  ordtcnv  20294  ordtrest2  20297  utop2nei  21343  utop3cls  21344  dvlt0  23036  dvcnvrelem1  23048  ofpreima  28343  funcnvmptOLD  28345  funcnvmpt  28346  xrge0infssOLD  28416  oduprs  28492  odutos  28499  tosglblem  28505  ordtcnvNEW  28800  ordtrest2NEW  28803  xrge0iifiso  28815  omssubaddlemOLD  29204  omssubaddOLD  29205  ballotlemfrcn0OLD  29473  erdszelem9  29994  coepr  30463  dffr5  30464  dfso2  30465  cnvco1  30471  cnvco2  30472  pocnv  30475  socnv  30476  wzel  30578  wsuclem  30579  txpss3v  30716  brtxp  30718  brpprod3b  30725  idsset  30728  fixcnv  30746  brimage  30764  brcup  30777  brcap  30778  dfrecs2  30788  dfrdg4  30789  dfint3  30790  imagesset  30791  brlb  30793  fvline  30982  ellines  30990  trer  31043  gtinf  31046  poimirlem31  32035  poimir  32037  frinfm  32126  rencldnfilem  35734  cnvssco  36283  psshepw  36455  dffrege115  36645  frege131  36661  frege133  36663  infrglbOLD  37766  gte-lteh  40954  gt-lth  40955
  Copyright terms: Public domain W3C validator