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

Theorem brcnv 5034
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 5032 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 677 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    e. wcel 1869   _Vcvv 3082   class class class wbr 4421   `'ccnv 4850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-cnv 4859
This theorem is referenced by:  cnvco  5037  dfrn2  5040  dfdm4  5044  cnvsym  5231  intasym  5232  asymref  5233  qfto  5238  dminss  5267  imainss  5268  dminxp  5294  cnvcnv3  5302  cnvpo  5391  cnvso  5392  dffun2  5609  funcnvsn  5644  funcnv2  5658  fun2cnv  5661  imadif  5674  f1ompt  6057  foeqcnvco  6211  f1eqcocnv  6212  fliftcnv  6217  isocnv2  6235  fsplit  6910  ercnv  7390  ecid  7434  omxpenlem  7677  sbthcl  7698  fimax2g  7821  dfsup2  7962  eqinf  8004  infval  8006  infcllem  8007  wofib  8064  oemapso  8190  cflim2  8695  fin23lem40  8783  isfin1-3  8818  fin12  8845  negiso  10589  dfinfre  10590  dfinfmrOLD  10591  infrenegsup  10593  infmsupOLD  10594  infmrgelbOLD  10597  infmrlbOLD  10599  xrinfmss2  11598  xrinfm0OLD  11629  trclublem  13053  ramcl2lemOLD  14956  imasleval  15440  invsym2  15661  oppcsect2  15677  odupos  16374  oduposb  16375  oduglb  16378  odulub  16380  posglbd  16389  gsumcom3  19416  ordtbas2  20199  ordtcnv  20209  ordtrest2  20212  utop2nei  21257  utop3cls  21258  dvlt0  22949  dvcnvrelem1  22961  ofpreima  28264  funcnvmptOLD  28266  funcnvmpt  28267  xrge0infssOLD  28341  oduprs  28418  odutos  28425  tosglblem  28431  ordtcnvNEW  28728  ordtrest2NEW  28731  xrge0iifiso  28743  omssubaddlemOLD  29133  omssubaddOLD  29134  ballotlemfrcn0OLD  29402  erdszelem9  29924  coepr  30393  dffr5  30394  dfso2  30395  cnvco1  30401  cnvco2  30402  pocnv  30405  socnv  30406  wzel  30508  wsuclem  30509  txpss3v  30644  brtxp  30646  brpprod3b  30653  idsset  30656  fixcnv  30674  brimage  30692  brcup  30705  brcap  30706  dfrecs2  30716  dfrdg4  30717  dfint3  30718  imagesset  30719  brlb  30721  fvline  30910  ellines  30918  trer  30971  gtinf  30974  poimirlem31  31929  poimir  31931  frinfm  32020  rencldnfilem  35626  psshepw  36286  dffrege115  36476  frege131  36492  frege133  36494  infrglbOLD  37533  gte-lteh  39790  gt-lth  39791
  Copyright terms: Public domain W3C validator