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

Theorem brcnvg 5117
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 5116 . 2 ((𝐴𝐶𝐵𝐷) → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
2 df-br 4482 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 4482 . 2 (𝐵𝑅𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
41, 2, 33bitr4g 301 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝐵𝑅𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wcel 1938  cop 4034   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:  brcnv  5119  brelrng  5167  eliniseg  5304  relbrcnvg  5314  brcodir  5325  elpredg  5501  predep  5513  dffv2  6064  ersym  7516  brdifun  7533  eqinf  8148  inflb  8153  infglb  8154  infglbb  8155  infltoreq  8166  infempty  8170  lbinf  10725  lbinfmOLD  10726  infmrgelbOLD  10760  infmrlbOLD  10762  infmxrlbOLD  11906  infmxrgelbOLD  11907  brcnvtrclfv  13449  oduleg  16845  posglbd  16863  znleval  19626  brbtwn  25470  fcoinvbr  28588  xrge0infssdOLD  28709  infxrge0lbOLD  28713  infxrge0glbOLD  28715  cnvordtrestixx  29084  xrge0iifiso  29106  oms0OLD  29493  orvcgteel  29664  ballotlemircOLD  29766  inffz  30711  fv1stcnv  30768  fv2ndcnv  30769  wsuclem  30854  wsuclb  30857  colineardim1  31174  gtinf  31319  brnonrel  36796  ntrneifv2  37280  gte-lte  42317  gt-lt  42318
  Copyright terms: Public domain W3C validator