Theorem brcnv 5907

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 5904	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3488   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:  cnvco  5910  dfrn2  5913  dfdm4  5920  cnvsym  6144  cnvsymOLD  6145  cnvsymOLDOLD  6146  intasym  6147  asymref  6148  qfto  6153  dminss  6184  imainss  6185  dminxp  6211  cnvcnv3  6219  cnvpo  6318  cnvso  6319  dffun2  6583  dffun2OLD  6584  dffun2OLDOLD  6585  funcnvsn  6628  funcnv2  6646  fun2cnv  6649  imadif  6662  f1ompt  7145  foeqcnvco  7336  f1eqcocnv  7337  fliftcnv  7347  isocnv2  7367  fsplit  8158  ercnv  8784  ecid  8840  omxpenlem  9139  sbthcl  9161  fimax2g  9350  dfsup2  9513  eqinf  9553  infval  9555  infcllem  9556  wofib  9614  oemapso  9751  cflim2  10332  fin23lem40  10420  isfin1-3  10455  fin12  10482  negiso  12275  dfinfre  12276  infrenegsup  12278  xrinfmss2  13373  trclublem  15044  imasleval  17601  invsym2  17824  oppcsect2  17840  odupos  18398  oduposb  18399  odulub  18477  oduglb  18479  posglbdg  18485  gsumcom3  20020  ordtbas2  23220  ordtcnv  23230  ordtrest2  23233  utop2nei  24280  utop3cls  24281  dvlt0  26064  dvcnvrelem1  26076  nomaxmo  27761  ofpreima  32683  funcnvmpt  32685  oduprs  32937  odutos  32941  tosglblem  32947  mgccnv  32972  ordtcnvNEW  33866  ordtrest2NEW  33869  xrge0iifiso  33881  erdszelem9  35167  coepr  35715  dffr5  35716  dfso2  35717  cnvco1  35721  cnvco2  35722  pocnv  35725  txpss3v  35842  brtxp  35844  brpprod3b  35851  idsset  35854  fixcnv  35872  brimage  35890  brcup  35903  brcap  35904  dfrecs2  35914  dfrdg4  35915  dfint3  35916  imagesset  35917  brlb  35919  fvline  36108  ellines  36116  trer  36282  poimirlem31  37611  poimir  37613  frinfm  37695  xrnss3v  38328  rencldnfilem  42776  cnvssco  43568  psshepw  43750  dffrege115  43940  frege131  43956  frege133  43958  gte-lteh  48818  gt-lth  48819