Theorem brcnvg 5600

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∈ wcel 2050   class class class wbr 4929  ^◡ccnv 5406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-cnv 5415

This theorem is referenced by:  opelcnvg  5601  brcnv  5603  brelrng  5654  eliniseg  5798  relbrcnvg  5808  brcodir  5819  elpredg  6000  predep  6012  dffv2  6584  ersym  8101  brdifun  8118  eqinf  8743  inflb  8748  infglb  8749  infglbb  8750  infltoreq  8761  infempty  8766  brcnvtrclfv  14224  oduleg  17600  posglbd  17618  znleval  20403  brbtwn  26388  fcoinvbr  30122  cnvordtrestixx  30806  xrge0iifiso  30828  orvcgteel  31377  fv1stcnv  32546  fv2ndcnv  32547  wsuclem  32639  wsuclb  32642  slenlt  32758  colineardim1  33049  eldmcnv  35054  ineccnvmo  35063  alrmomorn  35064  brxrn  35077  dfcoss3  35113  brcoss3  35129  brcosscnv  35163  cosscnvssid3  35167  cosscnvssid4  35168  brnonrel  39317  ntrneifv2  39799  gte-lte  44196  gt-lt  44197