Theorem brcnvg 5833

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  5834  brcnv  5836  brelrng  5894  elinisegg  6053  relbrcnvg  6065  brcodir  6080  predep  6291  dffv2  6938  ersym  8660  brdifun  8678  eqinf  9412  inflb  9417  infglb  9418  infglbb  9419  infltoreq  9431  infempty  9436  brcnvtrclfv  14946  oduleg  18232  posglbdg  18355  znleval  21497  slenlt  27698  brbtwn  28880  fcoinvbr  32585  cnvordtrestixx  33897  xrge0iifiso  33919  orvcgteel  34453  fv1stcnv  35758  fv2ndcnv  35759  wsuclem  35807  wsuclb  35810  colineardim1  36043  eldmcnv  38321  ineccnvmo  38333  alrmomorn  38334  brcnvin  38346  brxrn  38350  dfcoss3  38399  cosscnv  38401  brcoss3  38418  brcosscnv  38457  cosscnvssid3  38461  cosscnvssid4  38462  brnonrel  43572  ntrneifv2  44063  glbprlem  48947  gte-lte  49707  gt-lt  49708