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

Theorem brcnv 5275
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 5273 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 707 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 1987  Vcvv 3190   class class class wbr 4623  ccnv 5083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-cnv 5092
This theorem is referenced by:  cnvco  5278  dfrn2  5281  dfdm4  5286  cnvsym  5479  intasym  5480  asymref  5481  qfto  5486  dminss  5516  imainss  5517  dminxp  5543  cnvcnv3  5551  cnvpo  5642  cnvso  5643  dffun2  5867  funcnvsn  5904  funcnv2  5925  fun2cnv  5928  imadif  5941  f1ompt  6348  foeqcnvco  6520  f1eqcocnv  6521  fliftcnv  6526  isocnv2  6546  fsplit  7242  ercnv  7723  ecid  7772  omxpenlem  8021  sbthcl  8042  fimax2g  8166  dfsup2  8310  eqinf  8350  infval  8352  infcllem  8353  wofib  8410  oemapso  8539  cflim2  9045  fin23lem40  9133  isfin1-3  9168  fin12  9195  negiso  10963  dfinfre  10964  infrenegsup  10966  xrinfmss2  12100  trclublem  13684  imasleval  16141  invsym2  16363  oppcsect2  16379  odupos  17075  oduposb  17076  oduglb  17079  odulub  17081  posglbd  17090  gsumcom3  20145  ordtbas2  20935  ordtcnv  20945  ordtrest2  20948  utop2nei  21994  utop3cls  21995  dvlt0  23706  dvcnvrelem1  23718  ofpreima  29349  funcnvmptOLD  29351  funcnvmpt  29352  oduprs  29483  odutos  29490  tosglblem  29496  ordtcnvNEW  29790  ordtrest2NEW  29793  xrge0iifiso  29805  erdszelem9  30942  coepr  31403  dffr5  31404  dfso2  31405  cnvco1  31411  cnvco2  31412  pocnv  31415  socnv  31416  wzelOLD  31526  wsuclemOLD  31528  txpss3v  31680  brtxp  31682  brpprod3b  31689  idsset  31692  fixcnv  31710  brimage  31728  brcup  31741  brcap  31742  dfrecs2  31752  dfrdg4  31753  dfint3  31754  imagesset  31755  brlb  31757  fvline  31946  ellines  31954  trer  32005  gtinfOLD  32009  poimirlem31  33111  poimir  33113  frinfm  33201  rencldnfilem  36903  cnvssco  37432  psshepw  37603  dffrege115  37793  frege131  37809  frege133  37811  gte-lteh  41790  gt-lth  41791
  Copyright terms: Public domain W3C validator