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

Theorem brcnv 5047
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 5045 . 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 1725   _Vcvv 2948   class class class wbr 4204   `'ccnv 4869
This theorem is referenced by:  cnvco  5048  dfrn2  5051  dfdm4  5055  cnvsym  5240  intasym  5241  asymref  5242  qfto  5247  dminss  5278  imainss  5279  dminxp  5303  cnvcnv3  5312  cnvpo  5402  cnvso  5403  dffun2  5456  funcnvsn  5488  funcnv2  5502  fun2cnv  5505  imadif  5520  f1ompt  5883  foeqcnvco  6019  f1eqcocnv  6020  fliftcnv  6025  isocnv2  6043  fsplit  6443  ercnv  6918  ecid  6961  omxpenlem  7201  sbthcl  7221  fimax2g  7345  dfsup2  7439  dfsup2OLD  7440  wofib  7506  oemapso  7630  cflim2  8135  fin23lem40  8223  isfin1-3  8258  fin12  8285  negiso  9976  dfinfmr  9977  infmsup  9978  infmrgelb  9980  infmrlb  9981  xrinfmss2  10881  xrinfm0  10907  ramcl2lem  13369  imasleval  13758  invsym2  13980  oppcsect2  13992  odupos  14554  oduposb  14555  oduglb  14558  odulub  14560  posglbd  14568  ordtbas2  17247  ordtcnv  17257  ordtrest2  17260  utop2nei  18272  utop3cls  18273  dvlt0  19881  dvcnvrelem1  19893  ofpreima  24073  funcnvmptOLD  24074  funcnvmpt  24075  xrge0iifiso  24313  ballotlemfrcn0  24779  erdszelem9  24877  coepr  25367  dffr5  25368  dfso2  25369  cnvco1  25375  cnvco2  25376  pocnv  25379  socnv  25380  wzel  25567  wsuclem  25568  txpss3v  25715  brtxp  25717  brpprod3b  25724  idsset  25727  fixcnv  25745  brimage  25763  brcup  25776  brcap  25777  dfrdg4  25787  tfrqfree  25788  dfint3  25789  imagesset  25790  brlb  25792  fvline  26070  ellines  26078  trer  26310  gtinf  26313  frinfm  26428  rencldnfilem  26872  gsumcom3  27422  infrglb  27689  gte-lteh  28406  gt-lth  28407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-cnv 4878
  Copyright terms: Public domain W3C validator