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

Theorem brcnvg 5176
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 5175 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( <. A ,  B >.  e.  `' R  <->  <. B ,  A >.  e.  R ) )
2 df-br 4443 . 2  |-  ( A `' R B  <->  <. A ,  B >.  e.  `' R
)
3 df-br 4443 . 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 1762   <.cop 4028   class class class wbr 4442   `'ccnv 4993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443  df-opab 4501  df-cnv 5002
This theorem is referenced by:  brcnv  5178  brelrng  5225  eliniseg  5359  relbrcnvg  5368  brcodir  5379  dffv2  5933  ersym  7315  brdifun  7330  lbinfm  10487  infmrgelb  10514  infmrlb  10515  infmxrlb  11516  infmxrgelb  11517  oduleg  15610  posglbd  15628  znleval  18355  brbtwn  23873  fcoinvbr  27122  xrge0infssd  27237  tosglblem  27307  cnvordtrestixx  27519  xrge0iifiso  27541  oms0  27894  orvcgteel  28034  ballotlemirc  28098  inffz  28571  elpredg  28823  predep  28837  wsuclem  28946  wsuclb  28949  colineardim1  29276  gtinf  29703  infrglb  31097  gte-lte  32076  gt-lt  32077
  Copyright terms: Public domain W3C validator