Theorem brcnvg 5877

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2099   class class class wbr 5143  ^◡ccnv 5672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144  df-opab 5206  df-cnv 5681

This theorem is referenced by:  opelcnvg  5878  brcnv  5880  brelrng  5938  elinisegg  6092  relbrcnvg  6104  brcodir  6120  predep  6331  dffv2  6988  ersym  8731  brdifun  8748  eqinf  9502  inflb  9507  infglb  9508  infglbb  9509  infltoreq  9520  infempty  9525  brcnvtrclfv  14977  oduleg  18276  posglbdg  18401  znleval  21482  slenlt  27679  brbtwn  28704  fcoinvbr  32389  cnvordtrestixx  33509  xrge0iifiso  33531  orvcgteel  34082  fv1stcnv  35367  fv2ndcnv  35368  wsuclem  35416  wsuclb  35419  colineardim1  35652  eldmcnv  37812  ineccnvmo  37824  alrmomorn  37825  brcnvin  37837  brxrn  37841  dfcoss3  37881  cosscnv  37883  brcoss3  37900  brcosscnv  37939  cosscnvssid3  37943  cosscnvssid4  37944  brnonrel  43010  ntrneifv2  43501  glbprlem  47975  gte-lte  48146  gt-lt  48147