Theorem brcnvg 5787

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2110   class class class wbr 5079  ^◡ccnv 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-cnv 5598

This theorem is referenced by:  opelcnvg  5788  brcnv  5790  brelrng  5849  elinisegg  6000  relbrcnvg  6012  brcodir  6023  predep  6232  dffv2  6860  ersym  8493  brdifun  8510  eqinf  9221  inflb  9226  infglb  9227  infglbb  9228  infltoreq  9239  infempty  9244  brcnvtrclfv  14712  oduleg  18006  posglbdg  18131  znleval  20760  brbtwn  27265  fcoinvbr  30943  cnvordtrestixx  31859  xrge0iifiso  31881  orvcgteel  32430  fv1stcnv  33747  fv2ndcnv  33748  wsuclem  33815  wsuclb  33818  slenlt  33951  colineardim1  34359  eldmcnv  36476  ineccnvmo  36485  alrmomorn  36486  brxrn  36500  dfcoss3  36536  brcoss3  36552  brcosscnv  36586  cosscnvssid3  36590  cosscnvssid4  36591  brnonrel  41167  ntrneifv2  41660  glbprlem  46228  gte-lte  46395  gt-lt  46396