Theorem brcnvg 5777

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ^◡ccnv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588

This theorem is referenced by:  opelcnvg  5778  brcnv  5780  brelrng  5839  elinisegg  5990  relbrcnvg  6002  brcodir  6013  predep  6222  dffv2  6845  ersym  8468  brdifun  8485  eqinf  9173  inflb  9178  infglb  9179  infglbb  9180  infltoreq  9191  infempty  9196  brcnvtrclfv  14642  oduleg  17924  posglbdg  18048  znleval  20674  brbtwn  27170  fcoinvbr  30848  cnvordtrestixx  31765  xrge0iifiso  31787  orvcgteel  32334  fv1stcnv  33657  fv2ndcnv  33658  wsuclem  33746  wsuclb  33749  slenlt  33882  colineardim1  34290  eldmcnv  36407  ineccnvmo  36416  alrmomorn  36417  brxrn  36431  dfcoss3  36467  brcoss3  36483  brcosscnv  36517  cosscnvssid3  36521  cosscnvssid4  36522  brnonrel  41086  ntrneifv2  41579  glbprlem  46147  gte-lte  46312  gt-lt  46313