Theorem brcnvg 5749

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2110   class class class wbr 5065  ^◡ccnv 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066  df-opab 5128  df-cnv 5562

This theorem is referenced by:  opelcnvg  5750  brcnv  5752  brelrng  5810  eliniseg  5957  relbrcnvg  5967  brcodir  5978  elpredg  6161  predep  6173  dffv2  6755  ersym  8300  brdifun  8317  eqinf  8947  inflb  8952  infglb  8953  infglbb  8954  infltoreq  8965  infempty  8970  brcnvtrclfv  14362  oduleg  17741  posglbd  17759  znleval  20700  brbtwn  26684  fcoinvbr  30357  cnvordtrestixx  31156  xrge0iifiso  31178  orvcgteel  31725  fv1stcnv  33020  fv2ndcnv  33021  wsuclem  33112  wsuclb  33115  slenlt  33231  colineardim1  33522  eldmcnv  35601  ineccnvmo  35610  alrmomorn  35611  brxrn  35625  dfcoss3  35661  brcoss3  35677  brcosscnv  35711  cosscnvssid3  35715  cosscnvssid4  35716  brnonrel  39947  ntrneifv2  40428  gte-lte  44822  gt-lt  44823