Theorem brcnvg 5823

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.

Step	Hyp	Ref	Expression
1		breq2 5078	. 2 ⊢ (𝑥 = 𝐴 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐴))
2		breq1 5077	. 2 ⊢ (𝑦 = 𝐵 → (𝑦𝑅𝐴 ↔ 𝐵𝑅𝐴))
3		df-cnv 5628	. 2 ⊢ ◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝑅𝑥}
4	1, 2, 3	brabg 5483	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∈ wcel 2121   class class class wbr 5074  ^◡ccnv 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  opelcnvg  5824  brcnv  5826  brelrng  5889  elinisegg  6051  relbrcnvg  6063  brcodir  6075  predep  6284  dffv2  6925  ersym  8650  brdifun  8668  eqinf  9392  inflb  9397  infglb  9398  infglbb  9399  infltoreq  9411  infempty  9416  brcnvtrclfv  14960  oduleg  18251  posglbdg  18374  znleval  21532  lenlts  27736  brbtwn  28988  fcoinvbr  32696  cnvordtrestixx  34107  xrge0iifiso  34129  orvcgteel  34662  fv1stcnv  36018  fv2ndcnv  36019  wsuclem  36064  wsuclb  36067  colineardim1  36302  eldmcnv  38725  ineccnvmo  38737  alrmomorn  38738  brcnvin  38758  brxrn  38763  dfcoss3  38884  cosscnv  38886  brcoss3  38903  brcosscnv  38942  cosscnvssid3  38946  cosscnvssid4  38947  brnonrel  44046  ntrneifv2  44537  glbprlem  49467  gte-lte  50226  gt-lt  50227