Theorem brcnvg 5827

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 5101	. 2 ⊢ (𝑥 = 𝐴 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐴))
2		breq1 5100	. 2 ⊢ (𝑦 = 𝐵 → (𝑦𝑅𝐴 ↔ 𝐵𝑅𝐴))
3		df-cnv 5631	. 2 ⊢ ◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝑅𝑥}
4	1, 2, 3	brabg 5486	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5097  ^◡ccnv 5622

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-cnv 5631

This theorem is referenced by:  opelcnvg  5828  brcnv  5830  brelrng  5889  elinisegg  6051  relbrcnvg  6063  brcodir  6075  predep  6287  dffv2  6928  ersym  8648  brdifun  8666  eqinf  9390  inflb  9395  infglb  9396  infglbb  9397  infltoreq  9409  infempty  9414  brcnvtrclfv  14928  oduleg  18215  posglbdg  18338  znleval  21511  slenlt  27722  brbtwn  28953  fcoinvbr  32660  cnvordtrestixx  34049  xrge0iifiso  34071  orvcgteel  34604  fv1stcnv  35950  fv2ndcnv  35951  wsuclem  35996  wsuclb  35999  colineardim1  36234  eldmcnv  38515  ineccnvmo  38527  alrmomorn  38528  brcnvin  38548  brxrn  38553  dfcoss3  38674  cosscnv  38676  brcoss3  38693  brcosscnv  38732  cosscnvssid3  38736  cosscnvssid4  38737  brnonrel  43867  ntrneifv2  44358  glbprlem  49247  gte-lte  50006  gt-lt  50007