Theorem brcnvg 5833

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ^◡ccnv 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  opelcnvg  5834  brcnv  5836  brelrng  5894  elinisegg  6053  relbrcnvg  6065  brcodir  6080  predep  6291  dffv2  6938  ersym  8660  brdifun  8678  eqinf  9412  inflb  9417  infglb  9418  infglbb  9419  infltoreq  9431  infempty  9436  brcnvtrclfv  14945  oduleg  18231  posglbdg  18354  znleval  21496  slenlt  27697  brbtwn  28879  fcoinvbr  32584  cnvordtrestixx  33896  xrge0iifiso  33918  orvcgteel  34452  fv1stcnv  35757  fv2ndcnv  35758  wsuclem  35806  wsuclb  35809  colineardim1  36042  eldmcnv  38320  ineccnvmo  38332  alrmomorn  38333  brcnvin  38345  brxrn  38349  dfcoss3  38398  cosscnv  38400  brcoss3  38417  brcosscnv  38456  cosscnvssid3  38460  cosscnvssid4  38461  brnonrel  43571  ntrneifv2  44062  glbprlem  48946  gte-lte  49706  gt-lt  49707