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 206   ∧ wa 395   ∈ wcel 2114   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-pr 5364

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 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  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  5885  elinisegg  6047  relbrcnvg  6059  brcodir  6071  predep  6283  dffv2  6924  ersym  8645  brdifun  8663  eqinf  9387  inflb  9392  infglb  9393  infglbb  9394  infltoreq  9406  infempty  9411  brcnvtrclfv  14954  oduleg  18245  posglbdg  18368  znleval  21523  lenlts  27704  brbtwn  28956  fcoinvbr  32663  cnvordtrestixx  34045  xrge0iifiso  34067  orvcgteel  34600  fv1stcnv  35947  fv2ndcnv  35948  wsuclem  35993  wsuclb  35996  colineardim1  36231  eldmcnv  38654  ineccnvmo  38666  alrmomorn  38667  brcnvin  38687  brxrn  38692  dfcoss3  38813  cosscnv  38815  brcoss3  38832  brcosscnv  38871  cosscnvssid3  38875  cosscnvssid4  38876  brnonrel  44004  ntrneifv2  44495  glbprlem  49428  gte-lte  50187  gt-lt  50188