Theorem brcnvg 5865

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2141   class class class wbr 5108  ^◡ccnv 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-cnv 5669

This theorem is referenced by:  opelcnvg  5866  brcnv  5868  brelrng  5931  elinisegg  6095  relbrcnvg  6107  brcodir  6119  predep  6331  dffv2  6976  ersym  8706  brdifun  8724  eqinf  9444  inflb  9449  infglb  9450  infglbb  9451  infltoreq  9463  infempty  9468  brcnvtrclfv  15039  oduleg  18345  posglbdg  18468  znleval  21683  lenlts  27892  tgelrnpln  29032  brbtwn  29215  fcoinvbr  32916  cnvordtrestixx  34269  xrge0iifiso  34291  orvcgteel  34824  fv1stcnv  36223  fv2ndcnv  36224  wsuclem  36269  wsuclb  36272  colineardim1  36507  eldmcnv  38940  ineccnvmo  38952  alrmomorn  38953  brcnvin  38973  brxrn  38978  dfcoss3  39099  cosscnv  39101  brcoss3  39118  brcosscnv  39157  cosscnvssid3  39161  cosscnvssid4  39162  brnonrel  44263  ntrneifv2  44754  glbprlem  49688  gte-lte  50447  gt-lt  50448