Theorem brcnvg 5063

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 5062	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
2		df-br 4435	. 2 ⊢ (𝐴◡𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ◡𝑅)
3		df-br 4435	. 2 ⊢ (𝐵𝑅𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
4	1, 2, 3	3bitr4g 298	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))

Syntax hints:   → wi 4   ↔ wb 191   ∧ wa 378   ∈ wcel 1937  ⟨cop 4001   class class class wbr 4434  ^◡ccnv 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-br 4435  df-opab 4494  df-cnv 4888

This theorem is referenced by:  brcnv  5065  brelrng  5113  eliniseg  5247  relbrcnvg  5258  brcodir  5269  elpredg  5445  predep  5457  dffv2  6005  ersym  7452  brdifun  7469  eqinf  8083  inflb  8088  infglb  8089  infglbb  8090  infltoreq  8101  infempty  8105  lbinf  10648  lbinfmOLD  10649  infmrgelbOLD  10684  infmrlbOLD  10686  infmxrlbOLD  11719  infmxrgelbOLD  11720  brcnvtrclfv  13227  oduleg  16543  posglbd  16561  znleval  19283  brbtwn  25090  fcoinvbr  28373  xrge0infssdOLD  28499  infxrge0lbOLD  28503  infxrge0glbOLD  28505  cnvordtrestixx  28874  xrge0iifiso  28896  oms0OLD  29283  orvcgteel  29454  ballotlemircOLD  29556  inffz  30515  fv1stcnv  30573  fv2ndcnv  30574  wsuclem  30659  wsuclb  30662  colineardim1  30979  gtinf  31124  brnonrel  36434  ntrneifv2  36894  infrglbOLD  38071  gte-lte  41633  gt-lt  41634