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

Theorem brcnv 5119
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 5117 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 703 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1938  Vcvv 3077   class class class wbr 4481  ccnv 4931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-br 4482  df-opab 4542  df-cnv 4940
This theorem is referenced by:  cnvco  5122  dfrn2  5125  dfdm4  5129  cnvsym  5320  intasym  5321  asymref  5322  qfto  5327  dminss  5356  imainss  5357  dminxp  5383  cnvcnv3  5391  cnvpo  5480  cnvso  5481  dffun2  5699  funcnvsn  5735  funcnv2  5756  fun2cnv  5759  imadif  5772  f1ompt  6173  foeqcnvco  6331  f1eqcocnv  6332  fliftcnv  6337  isocnv2  6357  fsplit  7043  ercnv  7525  ecid  7574  omxpenlem  7821  sbthcl  7842  fimax2g  7966  dfsup2  8108  eqinf  8148  infval  8150  infcllem  8151  wofib  8208  oemapso  8337  cflim2  8843  fin23lem40  8931  isfin1-3  8966  fin12  8993  negiso  10753  dfinfre  10754  infrenegsup  10756  infmsupOLD  10757  infmrgelbOLD  10760  infmrlbOLD  10762  xrinfmss2  11878  trclublem  13439  imasleval  15914  invsym2  16136  oppcsect2  16152  odupos  16848  oduposb  16849  oduglb  16852  odulub  16854  posglbd  16863  gsumcom3  19925  ordtbas2  20706  ordtcnv  20716  ordtrest2  20719  utop2nei  21765  utop3cls  21766  dvlt0  23448  dvcnvrelem1  23460  ofpreima  28637  funcnvmptOLD  28639  funcnvmpt  28640  xrge0infssOLD  28707  oduprs  28783  odutos  28790  tosglblem  28796  ordtcnvNEW  29091  ordtrest2NEW  29094  xrge0iifiso  29106  omssubaddlemOLD  29495  omssubaddOLD  29496  ballotlemfrcn0OLD  29764  erdszelem9  30281  coepr  30738  dffr5  30739  dfso2  30740  cnvco1  30746  cnvco2  30747  pocnv  30750  socnv  30751  wzel  30853  wsuclem  30854  txpss3v  30991  brtxp  30993  brpprod3b  31000  idsset  31003  fixcnv  31021  brimage  31039  brcup  31052  brcap  31053  dfrecs2  31063  dfrdg4  31064  dfint3  31065  imagesset  31066  brlb  31068  fvline  31257  ellines  31265  trer  31316  gtinf  31319  poimirlem31  32485  poimir  32487  frinfm  32575  rencldnfilem  36277  cnvssco  36813  psshepw  36984  dffrege115  37174  frege131  37190  frege133  37192  gte-lteh  42319  gt-lth  42320
  Copyright terms: Public domain W3C validator