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

Theorem brcnvg 5718
 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 5037 . 2 (𝑥 = 𝐴 → (𝑦𝑅𝑥𝑦𝑅𝐴))
2 breq1 5036 . 2 (𝑦 = 𝐵 → (𝑦𝑅𝐴𝐵𝑅𝐴))
3 df-cnv 5531 . 2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝑅𝑥}
41, 2, 3brabg 5394 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝐵𝑅𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2112   class class class wbr 5033  ◡ccnv 5522 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-cnv 5531 This theorem is referenced by:  opelcnvg  5719  brcnv  5721  brelrng  5779  eliniseg  5929  relbrcnvg  5939  brcodir  5950  elpredg  6134  predep  6146  dffv2  6737  ersym  8288  brdifun  8305  eqinf  8936  inflb  8941  infglb  8942  infglbb  8943  infltoreq  8954  infempty  8959  brcnvtrclfv  14358  oduleg  17738  posglbd  17756  znleval  20250  brbtwn  26697  fcoinvbr  30375  cnvordtrestixx  31270  xrge0iifiso  31292  orvcgteel  31839  fv1stcnv  33134  fv2ndcnv  33135  wsuclem  33226  wsuclb  33229  slenlt  33345  colineardim1  33636  eldmcnv  35761  ineccnvmo  35770  alrmomorn  35771  brxrn  35785  dfcoss3  35821  brcoss3  35837  brcosscnv  35871  cosscnvssid3  35875  cosscnvssid4  35876  brnonrel  40286  ntrneifv2  40780  gte-lte  45247  gt-lt  45248
 Copyright terms: Public domain W3C validator