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

Theorem brcnv 5065
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 5063 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝐵𝑅𝐴))
41, 2, 3mp2an 695 1 (𝐴𝑅𝐵𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 191  wcel 1937  Vcvv 3066   class class class wbr 4434  ccnv 4879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-br 4435  df-opab 4494  df-cnv 4888
This theorem is referenced by:  cnvco  5068  dfrn2  5071  dfdm4  5075  cnvsym  5264  intasym  5265  asymref  5266  qfto  5271  dminss  5300  imainss  5301  dminxp  5327  cnvcnv3  5335  cnvpo  5425  cnvso  5426  dffun2  5643  funcnvsn  5679  funcnv2  5697  fun2cnv  5700  imadif  5713  f1ompt  6111  foeqcnvco  6269  f1eqcocnv  6270  fliftcnv  6275  isocnv2  6295  fsplit  6980  ercnv  7461  ecid  7510  omxpenlem  7757  sbthcl  7778  fimax2g  7902  dfsup2  8043  eqinf  8083  infval  8085  infcllem  8086  wofib  8143  oemapso  8272  cflim2  8778  fin23lem40  8866  isfin1-3  8901  fin12  8928  negiso  10676  dfinfre  10677  dfinfmrOLD  10678  infrenegsup  10680  infmsupOLD  10681  infmrgelbOLD  10684  infmrlbOLD  10686  xrinfmss2  11691  xrinfm0OLD  11722  trclublem  13217  ramcl2lemOLD  15125  imasleval  15612  invsym2  15834  oppcsect2  15850  odupos  16546  oduposb  16547  oduglb  16550  odulub  16552  posglbd  16561  gsumcom3  19582  ordtbas2  20364  ordtcnv  20374  ordtrest2  20377  utop2nei  21423  utop3cls  21424  dvlt0  23118  dvcnvrelem1  23130  ofpreima  28425  funcnvmptOLD  28427  funcnvmpt  28428  xrge0infssOLD  28497  oduprs  28573  odutos  28580  tosglblem  28586  ordtcnvNEW  28881  ordtrest2NEW  28884  xrge0iifiso  28896  omssubaddlemOLD  29285  omssubaddOLD  29286  ballotlemfrcn0OLD  29554  erdszelem9  30074  coepr  30543  dffr5  30544  dfso2  30545  cnvco1  30551  cnvco2  30552  pocnv  30555  socnv  30556  wzel  30658  wsuclem  30659  txpss3v  30796  brtxp  30798  brpprod3b  30805  idsset  30808  fixcnv  30826  brimage  30844  brcup  30857  brcap  30858  dfrecs2  30868  dfrdg4  30869  dfint3  30870  imagesset  30871  brlb  30873  fvline  31062  ellines  31070  trer  31121  gtinf  31124  poimirlem31  32209  poimir  32211  frinfm  32300  rencldnfilem  35903  cnvssco  36451  psshepw  36623  dffrege115  36813  frege131  36829  frege133  36831  infrglbOLD  38071  gte-lteh  41635  gt-lth  41636
  Copyright terms: Public domain W3C validator