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

Theorem brcnv 5214
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 5212 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 703 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1976  Vcvv 3171   class class class wbr 4576  ccnv 5026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2588  ax-sep 4702  ax-nul 4711  ax-pr 4827
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 1700  df-sb 1867  df-eu 2460  df-mo 2461  df-clab 2595  df-cleq 2601  df-clel 2604  df-nfc 2738  df-rab 2903  df-v 3173  df-dif 3541  df-un 3543  df-in 3545  df-ss 3552  df-nul 3873  df-if 4035  df-sn 4124  df-pr 4126  df-op 4130  df-br 4577  df-opab 4637  df-cnv 5035
This theorem is referenced by:  cnvco  5217  dfrn2  5220  dfdm4  5224  cnvsym  5415  intasym  5416  asymref  5417  qfto  5422  dminss  5451  imainss  5452  dminxp  5478  cnvcnv3  5486  cnvpo  5575  cnvso  5576  dffun2  5799  funcnvsn  5835  funcnv2  5856  fun2cnv  5859  imadif  5872  f1ompt  6274  foeqcnvco  6432  f1eqcocnv  6433  fliftcnv  6438  isocnv2  6458  fsplit  7145  ercnv  7626  ecid  7675  omxpenlem  7922  sbthcl  7943  fimax2g  8067  dfsup2  8209  eqinf  8249  infval  8251  infcllem  8252  wofib  8309  oemapso  8438  cflim2  8944  fin23lem40  9032  isfin1-3  9067  fin12  9094  negiso  10849  dfinfre  10850  infrenegsup  10852  xrinfmss2  11968  trclublem  13527  imasleval  15969  invsym2  16191  oppcsect2  16207  odupos  16903  oduposb  16904  oduglb  16907  odulub  16909  posglbd  16918  gsumcom3  19965  ordtbas2  20746  ordtcnv  20756  ordtrest2  20759  utop2nei  21805  utop3cls  21806  dvlt0  23488  dvcnvrelem1  23500  ofpreima  28653  funcnvmptOLD  28655  funcnvmpt  28656  oduprs  28792  odutos  28799  tosglblem  28805  ordtcnvNEW  29099  ordtrest2NEW  29102  xrge0iifiso  29114  erdszelem9  30240  coepr  30700  dffr5  30701  dfso2  30702  cnvco1  30708  cnvco2  30709  pocnv  30712  socnv  30713  wzelOLD  30821  wsuclemOLD  30823  txpss3v  30960  brtxp  30962  brpprod3b  30969  idsset  30972  fixcnv  30990  brimage  31008  brcup  31021  brcap  31022  dfrecs2  31032  dfrdg4  31033  dfint3  31034  imagesset  31035  brlb  31037  fvline  31226  ellines  31234  trer  31285  gtinfOLD  31289  poimirlem31  32412  poimir  32414  frinfm  32502  rencldnfilem  36204  cnvssco  36733  psshepw  36904  dffrege115  37094  frege131  37110  frege133  37112  gte-lteh  42228  gt-lth  42229
  Copyright terms: Public domain W3C validator