Theorem brcnvg 5843

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ^◡ccnv 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646

This theorem is referenced by:  opelcnvg  5844  brcnv  5846  brelrng  5905  elinisegg  6064  relbrcnvg  6076  brcodir  6092  predep  6303  dffv2  6956  ersym  8683  brdifun  8701  eqinf  9436  inflb  9441  infglb  9442  infglbb  9443  infltoreq  9455  infempty  9460  brcnvtrclfv  14969  oduleg  18251  posglbdg  18374  znleval  21464  slenlt  27664  brbtwn  28826  fcoinvbr  32534  cnvordtrestixx  33903  xrge0iifiso  33925  orvcgteel  34459  fv1stcnv  35764  fv2ndcnv  35765  wsuclem  35813  wsuclb  35816  colineardim1  36049  eldmcnv  38327  ineccnvmo  38339  alrmomorn  38340  brcnvin  38352  brxrn  38356  dfcoss3  38405  cosscnv  38407  brcoss3  38424  brcosscnv  38463  cosscnvssid3  38467  cosscnvssid4  38468  brnonrel  43578  ntrneifv2  44069  glbprlem  48953  gte-lte  49713  gt-lt  49714