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

Theorem brcnvg 4850
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 4849 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( <. A ,  B >.  e.  `' R  <->  <. B ,  A >.  e.  R ) )
2 df-br 3998 . 2  |-  ( A `' R B  <->  <. A ,  B >.  e.  `' R
)
3 df-br 3998 . 2  |-  ( B R A  <->  <. B ,  A >.  e.  R )
41, 2, 33bitr4g 281 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A `' R B 
<->  B R A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    e. wcel 1621   <.cop 3617   class class class wbr 3997   `'ccnv 4660
This theorem is referenced by:  brcnv  4852  brelrng  4896  eliniseg  5030  relbrcnvg  5040  brcodir  5050  dffv2  5526  ersym  6640  brdifun  6655  lbinfm  9675  infmrgelb  9702  infmrlb  9703  infmxrlb  10618  infmxrgelb  10619  oduleg  14198  posglbd  14215  znleval  16470  ballotlemirc  23051  inffz  23466  elpredg  23547  predep  23561  brbtwn  23902  colineardim1  24059  cnvref  24431  mnlmxl2  24636  nfwpr4c  24652  toplat  24657  gtinf  25601  gte-lte  27243  gt-lt  27244
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-br 3998  df-opab 4052  df-cnv 4677
  Copyright terms: Public domain W3C validator