Theorem brcnvg 5788

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   class class class wbr 5074  ^◡ccnv 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-cnv 5597

This theorem is referenced by:  opelcnvg  5789  brcnv  5791  brelrng  5850  elinisegg  6001  relbrcnvg  6013  brcodir  6024  predep  6233  dffv2  6863  ersym  8510  brdifun  8527  eqinf  9243  inflb  9248  infglb  9249  infglbb  9250  infltoreq  9261  infempty  9266  brcnvtrclfv  14714  oduleg  18008  posglbdg  18133  znleval  20762  brbtwn  27267  fcoinvbr  30947  cnvordtrestixx  31863  xrge0iifiso  31885  orvcgteel  32434  fv1stcnv  33751  fv2ndcnv  33752  wsuclem  33819  wsuclb  33822  slenlt  33955  colineardim1  34363  eldmcnv  36480  ineccnvmo  36489  alrmomorn  36490  brxrn  36504  dfcoss3  36540  brcoss3  36556  brcosscnv  36590  cosscnvssid3  36594  cosscnvssid4  36595  brnonrel  41197  ntrneifv2  41690  glbprlem  46259  gte-lte  46426  gt-lt  46427