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

Theorem brcnv 5227
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 5225 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 704 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wcel 1977  Vcvv 3173   class class class wbr 4583  ccnv 5037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046
This theorem is referenced by:  cnvco  5230  dfrn2  5233  dfdm4  5238  cnvsym  5429  intasym  5430  asymref  5431  qfto  5436  dminss  5466  imainss  5467  dminxp  5493  cnvcnv3  5501  cnvpo  5590  cnvso  5591  dffun2  5814  funcnvsn  5850  funcnv2  5871  fun2cnv  5874  imadif  5887  f1ompt  6290  foeqcnvco  6455  f1eqcocnv  6456  fliftcnv  6461  isocnv2  6481  fsplit  7169  ercnv  7650  ecid  7699  omxpenlem  7946  sbthcl  7967  fimax2g  8091  dfsup2  8233  eqinf  8273  infval  8275  infcllem  8276  wofib  8333  oemapso  8462  cflim2  8968  fin23lem40  9056  isfin1-3  9091  fin12  9118  negiso  10880  dfinfre  10881  infrenegsup  10883  xrinfmss2  12013  trclublem  13582  imasleval  16024  invsym2  16246  oppcsect2  16262  odupos  16958  oduposb  16959  oduglb  16962  odulub  16964  posglbd  16973  gsumcom3  20024  ordtbas2  20805  ordtcnv  20815  ordtrest2  20818  utop2nei  21864  utop3cls  21865  dvlt0  23572  dvcnvrelem1  23584  ofpreima  28848  funcnvmptOLD  28850  funcnvmpt  28851  oduprs  28987  odutos  28994  tosglblem  29000  ordtcnvNEW  29294  ordtrest2NEW  29297  xrge0iifiso  29309  erdszelem9  30435  coepr  30895  dffr5  30896  dfso2  30897  cnvco1  30903  cnvco2  30904  pocnv  30907  socnv  30908  wzelOLD  31016  wsuclemOLD  31018  txpss3v  31155  brtxp  31157  brpprod3b  31164  idsset  31167  fixcnv  31185  brimage  31203  brcup  31216  brcap  31217  dfrecs2  31227  dfrdg4  31228  dfint3  31229  imagesset  31230  brlb  31232  fvline  31421  ellines  31429  trer  31480  gtinfOLD  31484  poimirlem31  32610  poimir  32612  frinfm  32700  rencldnfilem  36402  cnvssco  36931  psshepw  37102  dffrege115  37292  frege131  37308  frege133  37310  gte-lteh  42266  gt-lth  42267
  Copyright terms: Public domain W3C validator