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

Theorem brcnv 5746
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 𝐴 ∈ V
opelcnv.2 𝐵 ∈ V
Assertion
Ref Expression
brcnv (𝐴𝑅𝐵𝐵𝑅𝐴)

Proof of Theorem brcnv
StepHypRef Expression
1 opelcnv.1 . 2 𝐴 ∈ V
2 opelcnv.2 . 2 𝐵 ∈ V
3 brcnvg 5743 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 688 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105  Vcvv 3492   class class class wbr 5057  ccnv 5547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-cnv 5556
This theorem is referenced by:  cnvco  5749  dfrn2  5752  dfdm4  5757  cnvsym  5967  intasym  5968  asymref  5969  qfto  5974  dminss  6003  imainss  6004  dminxp  6030  cnvcnv3  6038  cnvpo  6131  cnvso  6132  dffun2  6358  funcnvsn  6397  funcnv2  6415  fun2cnv  6418  imadif  6431  f1ompt  6867  foeqcnvco  7047  f1eqcocnv  7048  fliftcnv  7053  isocnv2  7073  fsplit  7801  fsplitOLD  7802  ercnv  8299  ecid  8351  omxpenlem  8606  sbthcl  8627  fimax2g  8752  dfsup2  8896  eqinf  8936  infval  8938  infcllem  8939  wofib  8997  oemapso  9133  cflim2  9673  fin23lem40  9761  isfin1-3  9796  fin12  9823  negiso  11609  dfinfre  11610  infrenegsup  11612  xrinfmss2  12692  trclublem  14343  imasleval  16802  invsym2  17021  oppcsect2  17037  odupos  17733  oduposb  17734  oduglb  17737  odulub  17739  posglbd  17748  gsumcom3  19027  ordtbas2  21727  ordtcnv  21737  ordtrest2  21740  utop2nei  22786  utop3cls  22787  dvlt0  24529  dvcnvrelem1  24541  ofpreima  30338  funcnvmpt  30340  oduprs  30570  odutos  30577  tosglblem  30583  ordtcnvNEW  31062  ordtrest2NEW  31065  xrge0iifiso  31077  erdszelem9  32343  coepr  32885  dffr5  32886  dfso2  32887  cnvco1  32892  cnvco2  32893  pocnv  32896  nomaxmo  33098  txpss3v  33236  brtxp  33238  brpprod3b  33245  idsset  33248  fixcnv  33266  brimage  33284  brcup  33297  brcap  33298  dfrecs2  33308  dfrdg4  33309  dfint3  33310  imagesset  33311  brlb  33313  fvline  33502  ellines  33510  trer  33561  poimirlem31  34804  poimir  34806  frinfm  34891  xrnss3v  35504  rencldnfilem  39295  cnvssco  39844  psshepw  40012  dffrege115  40202  frege131  40218  frege133  40220  gte-lteh  44753  gt-lth  44754
  Copyright terms: Public domain W3C validator