Theorem brcnv 5895

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

Syntax hints:   ↔ wb 206   ∈ wcel 2105  Vcvv 3477   class class class wbr 5147  ^◡ccnv 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-cnv 5696

This theorem is referenced by:  cnvco  5898  dfrn2  5901  dfdm4  5908  cnvsym  6134  cnvsymOLD  6135  cnvsymOLDOLD  6136  intasym  6137  asymref  6138  qfto  6143  dminss  6174  imainss  6175  dminxp  6201  cnvcnv3  6209  cnvpo  6308  cnvso  6309  dffun2  6572  dffun2OLD  6573  dffun2OLDOLD  6574  funcnvsn  6617  funcnv2  6635  fun2cnv  6638  imadif  6651  f1ompt  7130  foeqcnvco  7319  f1eqcocnv  7320  fliftcnv  7330  isocnv2  7350  fsplit  8140  ercnv  8764  ecid  8820  omxpenlem  9111  sbthcl  9133  fimax2g  9319  dfsup2  9481  eqinf  9521  infval  9523  infcllem  9524  wofib  9582  oemapso  9719  cflim2  10300  fin23lem40  10388  isfin1-3  10423  fin12  10450  negiso  12245  dfinfre  12246  infrenegsup  12248  xrinfmss2  13349  trclublem  15030  imasleval  17587  invsym2  17810  oppcsect2  17826  oduprs  18357  odupos  18385  oduposb  18386  odulub  18464  oduglb  18466  posglbdg  18472  gsumcom3  20010  ordtbas2  23214  ordtcnv  23224  ordtrest2  23227  utop2nei  24274  utop3cls  24275  dvlt0  26058  dvcnvrelem1  26070  nomaxmo  27757  ofpreima  32681  funcnvmpt  32683  odutos  32942  tosglblem  32948  mgccnv  32973  ordtcnvNEW  33880  ordtrest2NEW  33883  xrge0iifiso  33895  erdszelem9  35183  coepr  35732  dffr5  35733  dfso2  35734  cnvco1  35738  cnvco2  35739  pocnv  35742  txpss3v  35859  brtxp  35861  brpprod3b  35868  idsset  35871  fixcnv  35889  brimage  35907  brcup  35920  brcap  35921  dfrecs2  35931  dfrdg4  35932  dfint3  35933  imagesset  35934  brlb  35936  fvline  36125  ellines  36133  trer  36298  poimirlem31  37637  poimir  37639  frinfm  37721  xrnss3v  38353  rencldnfilem  42807  cnvssco  43595  psshepw  43777  dffrege115  43967  frege131  43983  frege133  43985  gte-lteh  48956  gt-lth  48957