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

Theorem brcnv 5175
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 5173 . 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 1804   _Vcvv 3095   class class class wbr 4437   `'ccnv 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-cnv 4997
This theorem is referenced by:  cnvco  5178  dfrn2  5181  dfdm4  5185  cnvsym  5371  intasym  5372  asymref  5373  qfto  5378  dminss  5410  imainss  5411  dminxp  5437  cnvcnv3  5446  cnvpo  5535  cnvso  5536  dffun2  5588  funcnvsn  5623  funcnv2  5637  fun2cnv  5640  imadif  5653  f1ompt  6038  foeqcnvco  6188  f1eqcocnv  6189  fliftcnv  6194  isocnv2  6212  fsplit  6890  ercnv  7334  ecid  7378  omxpenlem  7620  sbthcl  7641  fimax2g  7768  dfsup2  7904  dfsup2OLD  7905  wofib  7973  oemapso  8104  cflim2  8646  fin23lem40  8734  isfin1-3  8769  fin12  8796  negiso  10526  dfinfmr  10527  infmsup  10528  infmrgelb  10530  infmrlb  10531  xrinfmss2  11513  xrinfm0  11539  ramcl2lem  14509  imasleval  14920  invsym2  15139  oppcsect2  15151  odupos  15744  oduposb  15745  oduglb  15748  odulub  15750  posglbd  15759  gsumcom3  18879  ordtbas2  19670  ordtcnv  19680  ordtrest2  19683  utop2nei  20731  utop3cls  20732  dvlt0  22384  dvcnvrelem1  22396  ofpreima  27485  funcnvmptOLD  27487  funcnvmpt  27488  xrge0infss  27558  oduprs  27622  odutos  27629  tosglblem  27635  ordtcnvNEW  27880  ordtrest2NEW  27883  xrge0iifiso  27895  ballotlemfrcn0  28446  erdszelem9  28621  coepr  29157  dffr5  29158  dfso2  29159  cnvco1  29165  cnvco2  29166  pocnv  29169  socnv  29170  wzel  29356  wsuclem  29357  txpss3v  29504  brtxp  29506  brpprod3b  29513  idsset  29516  fixcnv  29534  brimage  29552  brcup  29565  brcap  29566  dfrdg4  29576  tfrqfree  29577  dfint3  29578  imagesset  29579  brlb  29581  fvline  29770  ellines  29778  trer  30110  gtinf  30113  frinfm  30202  rencldnfilem  30730  lcmgcdlem  31188  infrglb  31538  gte-lteh  32990  gt-lth  32991  trclubg  37613  psshepw  37633
  Copyright terms: Public domain W3C validator