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

Theorem brcnvg 5787
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 5083 . 2 (𝑥 = 𝐴 → (𝑦𝑅𝑥𝑦𝑅𝐴))
2 breq1 5082 . 2 (𝑦 = 𝐵 → (𝑦𝑅𝐴𝐵𝑅𝐴))
3 df-cnv 5598 . 2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝑅𝑥}
41, 2, 3brabg 5455 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝐵𝑅𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wcel 2110   class class class wbr 5079  ccnv 5589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-cnv 5598
This theorem is referenced by:  opelcnvg  5788  brcnv  5790  brelrng  5849  elinisegg  6000  relbrcnvg  6012  brcodir  6023  predep  6232  dffv2  6860  ersym  8493  brdifun  8510  eqinf  9221  inflb  9226  infglb  9227  infglbb  9228  infltoreq  9239  infempty  9244  brcnvtrclfv  14712  oduleg  18006  posglbdg  18131  znleval  20760  brbtwn  27265  fcoinvbr  30943  cnvordtrestixx  31859  xrge0iifiso  31881  orvcgteel  32430  fv1stcnv  33747  fv2ndcnv  33748  wsuclem  33815  wsuclb  33818  slenlt  33951  colineardim1  34359  eldmcnv  36476  ineccnvmo  36485  alrmomorn  36486  brxrn  36500  dfcoss3  36536  brcoss3  36552  brcosscnv  36586  cosscnvssid3  36590  cosscnvssid4  36591  brnonrel  41167  ntrneifv2  41660  glbprlem  46228  gte-lte  46395  gt-lt  46396
  Copyright terms: Public domain W3C validator