Theorem brcnv 5862

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3459   class class class wbr 5119  ^◡ccnv 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-cnv 5662

This theorem is referenced by:  cnvco  5865  dfrn2  5868  dfdm4  5875  cnvsym  6101  cnvsymOLD  6102  cnvsymOLDOLD  6103  intasym  6104  asymref  6105  qfto  6110  dminss  6142  imainss  6143  dminxp  6169  cnvcnv3  6177  cnvpo  6276  cnvso  6277  dffun2  6540  dffun2OLD  6541  dffun2OLDOLD  6542  funcnvsn  6585  funcnv2  6603  fun2cnv  6606  imadif  6619  f1ompt  7100  foeqcnvco  7292  f1eqcocnv  7293  fliftcnv  7303  isocnv2  7323  fsplit  8114  ercnv  8738  ecid  8794  omxpenlem  9085  sbthcl  9107  fimax2g  9292  dfsup2  9454  eqinf  9495  infval  9497  infcllem  9498  wofib  9557  oemapso  9694  cflim2  10275  fin23lem40  10363  isfin1-3  10398  fin12  10425  negiso  12220  dfinfre  12221  infrenegsup  12223  xrinfmss2  13325  trclublem  15012  imasleval  17553  invsym2  17774  oppcsect2  17790  oduprs  18310  odupos  18336  oduposb  18337  odulub  18415  oduglb  18417  posglbdg  18423  gsumcom3  19957  ordtbas2  23127  ordtcnv  23137  ordtrest2  23140  utop2nei  24187  utop3cls  24188  dvlt0  25960  dvcnvrelem1  25972  nomaxmo  27660  ofpreima  32589  funcnvmpt  32591  odutos  32894  tosglblem  32900  mgccnv  32925  ordtcnvNEW  33897  ordtrest2NEW  33900  xrge0iifiso  33912  erdszelem9  35167  coepr  35716  dffr5  35717  dfso2  35718  cnvco1  35722  cnvco2  35723  pocnv  35726  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  36280  poimirlem31  37621  poimir  37623  frinfm  37705  xrnss3v  38336  rencldnfilem  42790  cnvssco  43577  psshepw  43759  dffrege115  43949  frege131  43965  frege133  43967  brpermmodel  44976  lambert0  46867  lamberte  46868  gte-lteh  49538  gt-lth  49539