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

Theorem brcnvg 5877
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
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5147 . 2 (𝑥 = 𝐴 → (𝑦𝑅𝑥𝑦𝑅𝐴))
2 breq1 5146 . 2 (𝑦 = 𝐵 → (𝑦𝑅𝐴𝐵𝑅𝐴))
3 df-cnv 5681 . 2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝑅𝑥}
41, 2, 3brabg 5536 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝐵𝑅𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wcel 2099   class class class wbr 5143  ccnv 5672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144  df-opab 5206  df-cnv 5681
This theorem is referenced by:  opelcnvg  5878  brcnv  5880  brelrng  5938  elinisegg  6092  relbrcnvg  6104  brcodir  6120  predep  6331  dffv2  6988  ersym  8731  brdifun  8748  eqinf  9502  inflb  9507  infglb  9508  infglbb  9509  infltoreq  9520  infempty  9525  brcnvtrclfv  14977  oduleg  18276  posglbdg  18401  znleval  21482  slenlt  27679  brbtwn  28704  fcoinvbr  32389  cnvordtrestixx  33509  xrge0iifiso  33531  orvcgteel  34082  fv1stcnv  35367  fv2ndcnv  35368  wsuclem  35416  wsuclb  35419  colineardim1  35652  eldmcnv  37812  ineccnvmo  37824  alrmomorn  37825  brcnvin  37837  brxrn  37841  dfcoss3  37881  cosscnv  37883  brcoss3  37900  brcosscnv  37939  cosscnvssid3  37943  cosscnvssid4  37944  brnonrel  43010  ntrneifv2  43501  glbprlem  47975  gte-lte  48146  gt-lt  48147
  Copyright terms: Public domain W3C validator