Theorem brcnvg 5846

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

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

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-cnv 5649

This theorem is referenced by:  opelcnvg  5847  brcnv  5849  brelrng  5908  elinisegg  6067  relbrcnvg  6079  brcodir  6095  predep  6306  dffv2  6959  ersym  8686  brdifun  8704  eqinf  9443  inflb  9448  infglb  9449  infglbb  9450  infltoreq  9462  infempty  9467  brcnvtrclfv  14976  oduleg  18258  posglbdg  18381  znleval  21471  slenlt  27671  brbtwn  28833  fcoinvbr  32541  cnvordtrestixx  33910  xrge0iifiso  33932  orvcgteel  34466  fv1stcnv  35771  fv2ndcnv  35772  wsuclem  35820  wsuclb  35823  colineardim1  36056  eldmcnv  38334  ineccnvmo  38346  alrmomorn  38347  brcnvin  38359  brxrn  38363  dfcoss3  38412  cosscnv  38414  brcoss3  38431  brcosscnv  38470  cosscnvssid3  38474  cosscnvssid4  38475  brnonrel  43585  ntrneifv2  44076  glbprlem  48957  gte-lte  49717  gt-lt  49718