Theorem brcnvg 5750

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114   class class class wbr 5066  ^◡ccnv 5554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-cnv 5563

This theorem is referenced by:  opelcnvg  5751  brcnv  5753  brelrng  5811  eliniseg  5958  relbrcnvg  5968  brcodir  5979  elpredg  6162  predep  6174  dffv2  6756  ersym  8301  brdifun  8318  eqinf  8948  inflb  8953  infglb  8954  infglbb  8955  infltoreq  8966  infempty  8971  brcnvtrclfv  14363  oduleg  17742  posglbd  17760  znleval  20701  brbtwn  26685  fcoinvbr  30358  cnvordtrestixx  31156  xrge0iifiso  31178  orvcgteel  31725  fv1stcnv  33020  fv2ndcnv  33021  wsuclem  33112  wsuclb  33115  slenlt  33231  colineardim1  33522  eldmcnv  35617  ineccnvmo  35626  alrmomorn  35627  brxrn  35641  dfcoss3  35677  brcoss3  35693  brcosscnv  35727  cosscnvssid3  35731  cosscnvssid4  35732  brnonrel  39969  ntrneifv2  40450  gte-lte  44843  gt-lt  44844