Theorem brcnv 5826

Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)

Hypotheses

Ref	Expression
opelcnv.1	⊢ 𝐴 ∈ V
opelcnv.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
brcnv	⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)

Proof of Theorem brcnv

Step	Hyp	Ref	Expression
1		opelcnv.1	. 2 ⊢ 𝐴 ∈ V
2		opelcnv.2	. 2 ⊢ 𝐵 ∈ V
3		brcnvg 5823	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3427   class class class wbr 5074  ^◡ccnv 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  cnvco  5829  dfrn2  5832  dfdm4  5839  cnvsym  6066  intasym  6067  asymref  6068  qfto  6073  dminss  6106  imainss  6107  dminxp  6133  cnvcnv3  6141  cnvpo  6240  cnvso  6241  dffun2  6497  funcnvsn  6537  funcnv2  6555  fun2cnv  6558  imadif  6571  funcnvmpt  6938  f1ompt  7052  foeqcnvco  7244  f1eqcocnv  7245  fliftcnv  7255  isocnv2  7275  fsplit  8056  ercnv  8654  ecid  8716  omxpenlem  9005  sbthcl  9026  fimax2g  9185  dfsup2  9346  eqinf  9387  infval  9389  infcllem  9390  wofib  9449  oemapso  9592  cflim2  10174  fin23lem40  10262  isfin1-3  10297  fin12  10324  negiso  12125  dfinfre  12126  infrenegsup  12128  xrinfmss2  13252  trclublem  14946  imasleval  17494  invsym2  17719  oppcsect2  17735  oduprs  18255  odupos  18281  oduposb  18282  odulub  18360  oduglb  18362  posglbdg  18368  chnrev  18582  gsumcom3  19942  ordtbas2  23144  ordtcnv  23154  ordtrest2  23157  utop2nei  24203  utop3cls  24204  dvlt0  25960  dvcnvrelem1  25972  nomaxmo  27650  ofpreima  32726  odutos  33016  tosglblem  33022  mgccnv  33047  ordtcnvNEW  34052  ordtrest2NEW  34055  xrge0iifiso  34067  erdszelem9  35369  coepr  35923  dffr5  35924  dfso2  35925  cnvco1  35929  cnvco2  35930  pocnv  35933  txpss3v  36046  brtxp  36048  brpprod3b  36055  idsset  36058  fixcnv  36076  brimage  36094  brcup  36107  brcap  36108  dfrecs2  36120  dfrdg4  36121  dfint3  36122  imagesset  36123  brlb  36125  fvline  36314  ellines  36322  trer  36486  poimirlem31  37960  poimir  37962  frinfm  38044  xrnss3v  38690  rencldnfilem  43236  cnvssco  44021  psshepw  44203  dffrege115  44393  frege131  44409  frege133  44411  brpermmodel  45418  lambert0  47323  lamberte  47324  gte-lteh  50189  gt-lth  50190