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

Theorem brcnvg 5118
Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
Assertion
Ref Expression
brcnvg  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A `' R B 
<->  B R A ) )

Proof of Theorem brcnvg
StepHypRef Expression
1 opelcnvg 5117 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( <. A ,  B >.  e.  `' R  <->  <. B ,  A >.  e.  R ) )
2 df-br 4391 . 2  |-  ( A `' R B  <->  <. A ,  B >.  e.  `' R
)
3 df-br 4391 . 2  |-  ( B R A  <->  <. B ,  A >.  e.  R )
41, 2, 33bitr4g 288 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A `' R B 
<->  B R A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1758   <.cop 3981   class class class wbr 4390   `'ccnv 4937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391  df-opab 4449  df-cnv 4946
This theorem is referenced by:  brcnv  5120  brelrng  5167  eliniseg  5296  relbrcnvg  5305  brcodir  5315  dffv2  5863  ersym  7213  brdifun  7228  lbinfm  10384  infmrgelb  10411  infmrlb  10412  infmxrlb  11397  infmxrgelb  11398  oduleg  15404  posglbd  15422  znleval  18096  brbtwn  23280  xrge0infssd  26188  tosglblem  26264  cnvordtrestixx  26477  xrge0iifiso  26499  oms0  26844  orvcgteel  26984  ballotlemirc  27048  inffz  27521  elpredg  27773  predep  27787  wsuclem  27896  wsuclb  27899  colineardim1  28226  gtinf  28652  infrglb  29909  gte-lte  31355  gt-lt  31356
  Copyright terms: Public domain W3C validator