Theorem brcnv 5841

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100  ^◡ccnv 5633

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 2709  ax-sep 5245  ax-pr 5381

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5642

This theorem is referenced by:  cnvco  5844  dfrn2  5847  dfdm4  5854  cnvsym  6081  intasym  6082  asymref  6083  qfto  6088  dminss  6121  imainss  6122  dminxp  6148  cnvcnv3  6156  cnvpo  6255  cnvso  6256  dffun2  6512  funcnvsn  6552  funcnv2  6570  fun2cnv  6573  imadif  6586  funcnvmpt  6953  f1ompt  7067  foeqcnvco  7258  f1eqcocnv  7259  fliftcnv  7269  isocnv2  7289  fsplit  8071  ercnv  8669  ecid  8731  omxpenlem  9020  sbthcl  9041  fimax2g  9200  dfsup2  9361  eqinf  9402  infval  9404  infcllem  9405  wofib  9464  oemapso  9605  cflim2  10187  fin23lem40  10275  isfin1-3  10310  fin12  10337  negiso  12136  dfinfre  12137  infrenegsup  12139  xrinfmss2  13240  trclublem  14932  imasleval  17476  invsym2  17701  oppcsect2  17717  oduprs  18237  odupos  18263  oduposb  18264  odulub  18342  oduglb  18344  posglbdg  18350  chnrev  18564  gsumcom3  19924  ordtbas2  23152  ordtcnv  23162  ordtrest2  23165  utop2nei  24211  utop3cls  24212  dvlt0  25983  dvcnvrelem1  25995  nomaxmo  27683  ofpreima  32761  odutos  33067  tosglblem  33073  mgccnv  33098  ordtcnvNEW  34104  ordtrest2NEW  34107  xrge0iifiso  34119  erdszelem9  35421  coepr  35975  dffr5  35976  dfso2  35977  cnvco1  35981  cnvco2  35982  pocnv  35985  txpss3v  36098  brtxp  36100  brpprod3b  36107  idsset  36110  fixcnv  36128  brimage  36146  brcup  36159  brcap  36160  dfrecs2  36172  dfrdg4  36173  dfint3  36174  imagesset  36175  brlb  36177  fvline  36366  ellines  36374  trer  36538  poimirlem31  37931  poimir  37933  frinfm  38015  xrnss3v  38661  rencldnfilem  43206  cnvssco  43991  psshepw  44173  dffrege115  44363  frege131  44379  frege133  44381  brpermmodel  45388  lambert0  47276  lamberte  47277  gte-lteh  50114  gt-lth  50115