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

Theorem brcnvg 5063
Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
Assertion
Ref Expression
brcnvg ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝐵𝑅𝐴))

Proof of Theorem brcnvg
StepHypRef Expression
1 opelcnvg 5062 . 2 ((𝐴𝐶𝐵𝐷) → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
2 df-br 4435 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 4435 . 2 (𝐵𝑅𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
41, 2, 33bitr4g 298 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝐵𝑅𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  wa 378  wcel 1937  cop 4001   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:  brcnv  5065  brelrng  5113  eliniseg  5247  relbrcnvg  5258  brcodir  5269  elpredg  5445  predep  5457  dffv2  6005  ersym  7452  brdifun  7469  eqinf  8083  inflb  8088  infglb  8089  infglbb  8090  infltoreq  8101  infempty  8105  lbinf  10648  lbinfmOLD  10649  infmrgelbOLD  10684  infmrlbOLD  10686  infmxrlbOLD  11719  infmxrgelbOLD  11720  brcnvtrclfv  13227  oduleg  16543  posglbd  16561  znleval  19283  brbtwn  25090  fcoinvbr  28373  xrge0infssdOLD  28499  infxrge0lbOLD  28503  infxrge0glbOLD  28505  cnvordtrestixx  28874  xrge0iifiso  28896  oms0OLD  29283  orvcgteel  29454  ballotlemircOLD  29556  inffz  30515  fv1stcnv  30573  fv2ndcnv  30574  wsuclem  30659  wsuclb  30662  colineardim1  30979  gtinf  31124  brnonrel  36434  ntrneifv2  36894  infrglbOLD  38071  gte-lte  41633  gt-lt  41634
  Copyright terms: Public domain W3C validator