Theorem brcnvg 5856

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  ^◡ccnv 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-cnv 5658

This theorem is used by:  opelcnvg  5857  brcnv  5859  brelrng  5922  elinisegg  6090  relbrcnvg  6100  brcodir  6112  predep  6333  dffv2  6980  ersym  8730  brdifun  8748  eqinf  9477  inflb  9482  infglb  9483  infglbb  9484  infltoreq  9496  infempty  9501  brcnvtrclfv  15156  oduleg  18464  posglbdg  18587  znleval  21860  lenlts  28109  tgelrnpln  29254  brbtwn  29477  fcoinvbr  33199  cnvordtrestixx  34545  xrge0iifiso  34567  orvcgteel  35100  fv1stcnv  36541  fv2ndcnv  36542  wsuclem  36587  wsuclb  36590  colineardim1  36826  eldmcnv  39278  ineccnvmo  39290  alrmomorn  39291  brcnvin  39311  brxrn  39316  dfcoss3  39437  cosscnv  39439  brcoss3  39456  brcosscnv  39495  cosscnvssid3  39499  cosscnvssid4  39500  brnonrel  44589  ntrneifv2  45080  glbprlem  50073  gte-lte  50817  gt-lt  50818