Theorem brcnvg 5904

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ^◡ccnv 5699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708

This theorem is referenced by:  opelcnvg  5905  brcnv  5907  brelrng  5966  elinisegg  6123  relbrcnvg  6135  brcodir  6151  predep  6362  dffv2  7017  ersym  8775  brdifun  8793  eqinf  9553  inflb  9558  infglb  9559  infglbb  9560  infltoreq  9571  infempty  9576  brcnvtrclfv  15052  oduleg  18360  posglbdg  18485  znleval  21596  slenlt  27815  brbtwn  28932  fcoinvbr  32627  cnvordtrestixx  33859  xrge0iifiso  33881  orvcgteel  34432  fv1stcnv  35740  fv2ndcnv  35741  wsuclem  35789  wsuclb  35792  colineardim1  36025  eldmcnv  38301  ineccnvmo  38313  alrmomorn  38314  brcnvin  38326  brxrn  38330  dfcoss3  38370  cosscnv  38372  brcoss3  38389  brcosscnv  38428  cosscnvssid3  38432  cosscnvssid4  38433  brnonrel  43551  ntrneifv2  44042  glbprlem  48645  gte-lte  48816  gt-lt  48817