Theorem brcnvg 5834

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

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

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  opelcnvg  5835  brcnv  5837  brelrng  5895  elinisegg  6054  relbrcnvg  6066  brcodir  6081  predep  6292  dffv2  6939  ersym  8661  brdifun  8679  eqinf  9413  inflb  9418  infglb  9419  infglbb  9420  infltoreq  9432  infempty  9437  brcnvtrclfv  14947  oduleg  18233  posglbdg  18356  znleval  21498  slenlt  27699  brbtwn  28881  fcoinvbr  32586  cnvordtrestixx  33898  xrge0iifiso  33920  orvcgteel  34454  fv1stcnv  35759  fv2ndcnv  35760  wsuclem  35808  wsuclb  35811  colineardim1  36044  eldmcnv  38322  ineccnvmo  38334  alrmomorn  38335  brcnvin  38347  brxrn  38351  dfcoss3  38400  cosscnv  38402  brcoss3  38419  brcosscnv  38458  cosscnvssid3  38462  cosscnvssid4  38463  brnonrel  43573  ntrneifv2  44064  glbprlem  48948  gte-lte  49708  gt-lt  49709