Theorem brcnvg 5861

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ^◡ccnv 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663

This theorem is used by:  opelcnvg  5862  brcnv  5864  brelrng  5927  elinisegg  6091  relbrcnvg  6103  brcodir  6115  predep  6330  dffv2  6976  ersym  8716  brdifun  8734  eqinf  9462  inflb  9467  infglb  9468  infglbb  9469  infltoreq  9481  infempty  9486  brcnvtrclfv  15101  oduleg  18403  posglbdg  18526  znleval  21799  lenlts  28020  tgelrnpln  29165  brbtwn  29388  fcoinvbr  33110  cnvordtrestixx  34456  xrge0iifiso  34478  orvcgteel  35012  fv1stcnv  36439  fv2ndcnv  36440  wsuclem  36485  wsuclb  36488  colineardim1  36724  eldmcnv  39158  ineccnvmo  39170  alrmomorn  39171  brcnvin  39191  brxrn  39196  dfcoss3  39317  cosscnv  39319  brcoss3  39336  brcosscnv  39375  cosscnvssid3  39379  cosscnvssid4  39380  brnonrel  44494  ntrneifv2  44985  glbprlem  49956  gte-lte  50715  gt-lt  50716