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

Theorem brcnv 5448
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 5446 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 710 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 2127  Vcvv 3328   class class class wbr 4792  ccnv 5253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-br 4793  df-opab 4853  df-cnv 5262
This theorem is referenced by:  cnvco  5451  dfrn2  5454  dfdm4  5459  cnvsym  5656  intasym  5657  asymref  5658  qfto  5663  dminss  5693  imainss  5694  dminxp  5720  cnvcnv3  5728  cnvpo  5822  cnvso  5823  dffun2  6047  funcnvsn  6085  funcnv2  6106  fun2cnv  6109  imadif  6122  f1ompt  6533  foeqcnvco  6706  f1eqcocnv  6707  fliftcnv  6712  isocnv2  6732  fsplit  7438  ercnv  7920  ecid  7967  omxpenlem  8214  sbthcl  8235  fimax2g  8359  dfsup2  8503  eqinf  8543  infval  8545  infcllem  8546  wofib  8603  oemapso  8740  cflim2  9248  fin23lem40  9336  isfin1-3  9371  fin12  9398  negiso  11166  dfinfre  11167  infrenegsup  11169  xrinfmss2  12305  trclublem  13906  imasleval  16374  invsym2  16595  oppcsect2  16611  odupos  17307  oduposb  17308  oduglb  17311  odulub  17313  posglbd  17322  gsumcom3  20378  ordtbas2  21168  ordtcnv  21178  ordtrest2  21181  utop2nei  22226  utop3cls  22227  dvlt0  23938  dvcnvrelem1  23950  ofpreima  29745  funcnvmptOLD  29747  funcnvmpt  29748  oduprs  29936  odutos  29943  tosglblem  29949  ordtcnvNEW  30246  ordtrest2NEW  30249  xrge0iifiso  30261  erdszelem9  31459  coepr  31920  dffr5  31921  dfso2  31922  cnvco1  31927  cnvco2  31928  pocnv  31931  nomaxmo  32124  txpss3v  32262  brtxp  32264  brpprod3b  32271  idsset  32274  fixcnv  32292  brimage  32310  brcup  32323  brcap  32324  dfrecs2  32334  dfrdg4  32335  dfint3  32336  imagesset  32337  brlb  32339  fvline  32528  ellines  32536  trer  32587  gtinfOLD  32591  poimirlem31  33722  poimir  33724  frinfm  33812  xrnss3v  34426  rencldnfilem  37855  cnvssco  38383  psshepw  38553  dffrege115  38743  frege131  38759  frege133  38761  gte-lteh  42949  gt-lth  42950
  Copyright terms: Public domain W3C validator