Theorem brcnv 5785

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106  Vcvv 3430   class class class wbr 5074  ^◡ccnv 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5222  ax-nul 5229  ax-pr 5351

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5075  df-opab 5137  df-cnv 5593

This theorem is referenced by:  cnvco  5788  dfrn2  5791  dfdm4  5798  cnvsym  6013  intasym  6014  asymref  6015  qfto  6020  dminss  6050  imainss  6051  dminxp  6077  cnvcnv3  6085  cnvpo  6184  cnvso  6185  dffun2  6437  funcnvsn  6477  funcnv2  6495  fun2cnv  6498  imadif  6511  f1ompt  6978  foeqcnvco  7165  f1eqcocnv  7166  f1eqcocnvOLD  7167  fliftcnv  7175  isocnv2  7195  fsplit  7945  fsplitOLD  7946  ercnv  8507  ecid  8559  omxpenlem  8848  sbthcl  8870  fimax2g  9048  dfsup2  9191  eqinf  9231  infval  9233  infcllem  9234  wofib  9292  oemapso  9428  cflim2  10007  fin23lem40  10095  isfin1-3  10130  fin12  10157  negiso  11943  dfinfre  11944  infrenegsup  11946  xrinfmss2  13033  trclublem  14694  imasleval  17240  invsym2  17463  oppcsect2  17479  odupos  18034  oduposb  18035  odulub  18113  oduglb  18115  posglbdg  18121  gsumcom3  19567  ordtbas2  22330  ordtcnv  22340  ordtrest2  22343  utop2nei  23390  utop3cls  23391  dvlt0  25157  dvcnvrelem1  25169  ofpreima  30988  funcnvmpt  30990  oduprs  31228  odutos  31232  tosglblem  31238  mgccnv  31263  ordtcnvNEW  31856  ordtrest2NEW  31859  xrge0iifiso  31871  erdszelem9  33147  coepr  33706  dffr5  33707  dfso2  33708  cnvco1  33712  cnvco2  33713  pocnv  33716  nomaxmo  33887  txpss3v  34166  brtxp  34168  brpprod3b  34175  idsset  34178  fixcnv  34196  brimage  34214  brcup  34227  brcap  34228  dfrecs2  34238  dfrdg4  34239  dfint3  34240  imagesset  34241  brlb  34243  fvline  34432  ellines  34440  trer  34491  poimirlem31  35794  poimir  35796  frinfm  35879  xrnss3v  36488  rencldnfilem  40628  cnvssco  41173  psshepw  41355  dffrege115  41545  frege131  41561  frege133  41563  gte-lteh  46384  gt-lth  46385