Theorem brcnvg 5450

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

Step	Hyp	Ref	Expression
1		opelcnvg 5449	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
2		df-br 4797	. 2 ⊢ (𝐴◡𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ◡𝑅)
3		df-br 4797	. 2 ⊢ (𝐵𝑅𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
4	1, 2, 3	3bitr4g 303	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∈ wcel 2131  ⟨cop 4319   class class class wbr 4796  ^◡ccnv 5257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797  df-opab 4857  df-cnv 5266

This theorem is referenced by:  brcnv  5452  brelrng  5502  eliniseg  5644  relbrcnvg  5654  brcodir  5665  elpredg  5847  predep  5859  dffv2  6425  ersym  7915  brdifun  7932  eqinf  8547  inflb  8552  infglb  8553  infglbb  8554  infltoreq  8565  infempty  8569  brcnvtrclfv  13935  oduleg  17325  posglbd  17343  znleval  20097  brbtwn  25970  fcoinvbr  29718  cnvordtrestixx  30260  xrge0iifiso  30282  orvcgteel  30830  inffzOLD  31914  fv1stcnv  31977  fv2ndcnv  31978  wsuclem  32068  wsuclb  32071  slenlt  32175  colineardim1  32466  gtinfOLD  32612  eldmcnv  34428  ineccnvmo  34437  alrmomorn  34438  brxrn  34451  dfcoss3  34487  brcoss3  34503  brcosscnv  34537  cosscnvssid3  34541  cosscnvssid4  34542  brnonrel  38389  ntrneifv2  38872  gte-lte  42970  gt-lt  42971