Theorem brcnvg 5864

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

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

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667

This theorem is referenced by:  opelcnvg  5865  brcnv  5867  brelrng  5926  elinisegg  6085  relbrcnvg  6097  brcodir  6113  predep  6324  dffv2  6979  ersym  8736  brdifun  8754  eqinf  9502  inflb  9507  infglb  9508  infglbb  9509  infltoreq  9521  infempty  9526  brcnvtrclfv  15027  oduleg  18307  posglbdg  18430  znleval  21520  slenlt  27721  brbtwn  28883  fcoinvbr  32591  cnvordtrestixx  33949  xrge0iifiso  33971  orvcgteel  34505  fv1stcnv  35799  fv2ndcnv  35800  wsuclem  35848  wsuclb  35851  colineardim1  36084  eldmcnv  38368  ineccnvmo  38380  alrmomorn  38381  brcnvin  38393  brxrn  38397  dfcoss3  38437  cosscnv  38439  brcoss3  38456  brcosscnv  38495  cosscnvssid3  38499  cosscnvssid4  38500  brnonrel  43580  ntrneifv2  44071  glbprlem  48906  gte-lte  49555  gt-lt  49556