Theorem brcnvg 5829

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

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

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 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

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 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-cnv 5633

This theorem is referenced by:  opelcnvg  5830  brcnv  5832  brelrng  5891  elinisegg  6053  relbrcnvg  6065  brcodir  6077  predep  6289  dffv2  6930  ersym  8651  brdifun  8669  eqinf  9393  inflb  9398  infglb  9399  infglbb  9400  infltoreq  9412  infempty  9417  brcnvtrclfv  14931  oduleg  18218  posglbdg  18341  znleval  21514  lenlts  27725  brbtwn  28977  fcoinvbr  32684  cnvordtrestixx  34083  xrge0iifiso  34105  orvcgteel  34638  fv1stcnv  35984  fv2ndcnv  35985  wsuclem  36030  wsuclb  36033  colineardim1  36268  eldmcnv  38559  ineccnvmo  38571  alrmomorn  38572  brcnvin  38592  brxrn  38597  dfcoss3  38718  cosscnv  38720  brcoss3  38737  brcosscnv  38776  cosscnvssid3  38780  cosscnvssid4  38781  brnonrel  43908  ntrneifv2  44399  glbprlem  49287  gte-lte  50046  gt-lt  50047