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

Theorem brcnv 5111
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 5109 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 670 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1836   _Vcvv 3047   class class class wbr 4380   `'ccnv 4925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pr 4614
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-br 4381  df-opab 4439  df-cnv 4934
This theorem is referenced by:  cnvco  5114  dfrn2  5117  dfdm4  5121  cnvsym  5307  intasym  5308  asymref  5309  qfto  5314  dminss  5343  imainss  5344  dminxp  5370  cnvcnv3  5378  cnvpo  5467  cnvso  5468  dffun2  5519  funcnvsn  5554  funcnv2  5568  fun2cnv  5571  imadif  5584  f1ompt  5968  foeqcnvco  6122  f1eqcocnv  6123  fliftcnv  6128  isocnv2  6146  fsplit  6822  ercnv  7268  ecid  7312  omxpenlem  7555  sbthcl  7576  fimax2g  7699  dfsup2  7835  dfsup2OLD  7836  wofib  7903  oemapso  8032  cflim2  8574  fin23lem40  8662  isfin1-3  8697  fin12  8724  negiso  10453  dfinfmr  10454  infmsup  10455  infmrgelb  10457  infmrlb  10458  xrinfmss2  11441  xrinfm0  11467  trclublem  12852  ramcl2lem  14548  imasleval  14967  invsym2  15188  oppcsect2  15204  odupos  15901  oduposb  15902  oduglb  15905  odulub  15907  posglbd  15916  gsumcom3  19005  ordtbas2  19797  ordtcnv  19807  ordtrest2  19810  utop2nei  20857  utop3cls  20858  dvlt0  22510  dvcnvrelem1  22522  ofpreima  27683  funcnvmptOLD  27685  funcnvmpt  27686  xrge0infss  27760  oduprs  27827  odutos  27834  tosglblem  27840  ordtcnvNEW  28087  ordtrest2NEW  28090  xrge0iifiso  28102  omssubaddlem  28462  omssubadd  28463  ballotlemfrcn0  28687  erdszelem9  28868  coepr  29383  dffr5  29384  dfso2  29385  cnvco1  29391  cnvco2  29392  pocnv  29395  socnv  29396  wzel  29581  wsuclem  29582  txpss3v  29717  brtxp  29719  brpprod3b  29726  idsset  29729  fixcnv  29747  brimage  29765  brcup  29778  brcap  29779  dfrdg4  29789  tfrqfree  29790  dfint3  29791  imagesset  29792  brlb  29794  fvline  29983  ellines  29991  trer  30336  gtinf  30339  frinfm  30428  rencldnfilem  30955  lcmgcdlem  31416  infrglb  31785  gte-lteh  33491  gt-lth  33492  psshepw  38318  dffrege115  38512  frege131  38528  frege133  38530
  Copyright terms: Public domain W3C validator