Theorem brcnvg 5845

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

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

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 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-cnv 5648

This theorem is referenced by:  opelcnvg  5846  brcnv  5848  brelrng  5907  elinisegg  6066  relbrcnvg  6078  brcodir  6094  predep  6305  dffv2  6958  ersym  8685  brdifun  8703  eqinf  9442  inflb  9447  infglb  9448  infglbb  9449  infltoreq  9461  infempty  9466  brcnvtrclfv  14975  oduleg  18257  posglbdg  18380  znleval  21470  slenlt  27670  brbtwn  28832  fcoinvbr  32540  cnvordtrestixx  33909  xrge0iifiso  33931  orvcgteel  34465  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  43571  ntrneifv2  44062  glbprlem  48941  gte-lte  49690  gt-lt  49691