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

Theorem brcnv 5022
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 5020 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A `' R B 
<->  B R A ) )
41, 2, 3mp2an 672 1  |-  ( A `' R B  <->  B R A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1756   _Vcvv 2972   class class class wbr 4292   `'ccnv 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-cnv 4848
This theorem is referenced by:  cnvco  5025  dfrn2  5028  dfdm4  5032  cnvsym  5212  intasym  5213  asymref  5214  qfto  5219  dminss  5251  imainss  5252  dminxp  5278  cnvcnv3  5287  cnvpo  5375  cnvso  5376  dffun2  5428  funcnvsn  5463  funcnv2  5477  fun2cnv  5480  imadif  5493  f1ompt  5865  foeqcnvco  5998  f1eqcocnv  5999  fliftcnv  6004  isocnv2  6022  fsplit  6677  ercnv  7122  ecid  7165  omxpenlem  7412  sbthcl  7433  fimax2g  7558  dfsup2  7692  dfsup2OLD  7693  wofib  7759  oemapso  7890  cflim2  8432  fin23lem40  8520  isfin1-3  8555  fin12  8582  negiso  10306  dfinfmr  10307  infmsup  10308  infmrgelb  10310  infmrlb  10311  xrinfmss2  11273  xrinfm0  11299  ramcl2lem  14070  imasleval  14479  invsym2  14701  oppcsect2  14713  odupos  15305  oduposb  15306  oduglb  15309  odulub  15311  posglbd  15320  gsumcom3  18299  ordtbas2  18795  ordtcnv  18805  ordtrest2  18808  utop2nei  19825  utop3cls  19826  dvlt0  21477  dvcnvrelem1  21489  ofpreima  25984  funcnvmptOLD  25986  funcnvmpt  25987  xrge0infss  26053  oduprs  26117  odutos  26124  ordtcnvNEW  26350  ordtrest2NEW  26353  xrge0iifiso  26365  ballotlemfrcn0  26912  erdszelem9  27087  coepr  27562  dffr5  27563  dfso2  27564  cnvco1  27570  cnvco2  27571  pocnv  27574  socnv  27575  wzel  27761  wsuclem  27762  txpss3v  27909  brtxp  27911  brpprod3b  27918  idsset  27921  fixcnv  27939  brimage  27957  brcup  27970  brcap  27971  dfrdg4  27981  tfrqfree  27982  dfint3  27983  imagesset  27984  brlb  27986  fvline  28175  ellines  28183  trer  28511  gtinf  28514  frinfm  28629  rencldnfilem  29159  infrglb  29771  gte-lteh  31061  gt-lth  31062
  Copyright terms: Public domain W3C validator