Theorem brcnv 5717

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

Syntax hints:   ↔ wb 209   ∈ wcel 2111  Vcvv 3441   class class class wbr 5030  ^◡ccnv 5518

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-cnv 5527

This theorem is referenced by:  cnvco  5720  dfrn2  5723  dfdm4  5728  cnvsym  5941  intasym  5942  asymref  5943  qfto  5948  dminss  5977  imainss  5978  dminxp  6004  cnvcnv3  6012  cnvpo  6106  cnvso  6107  dffun2  6334  funcnvsn  6374  funcnv2  6392  fun2cnv  6395  imadif  6408  f1ompt  6852  foeqcnvco  7034  f1eqcocnv  7035  f1eqcocnvOLD  7036  fliftcnv  7043  isocnv2  7063  fsplit  7795  fsplitOLD  7796  ercnv  8293  ecid  8345  omxpenlem  8601  sbthcl  8623  fimax2g  8748  dfsup2  8892  eqinf  8932  infval  8934  infcllem  8935  wofib  8993  oemapso  9129  cflim2  9674  fin23lem40  9762  isfin1-3  9797  fin12  9824  negiso  11608  dfinfre  11609  infrenegsup  11611  xrinfmss2  12692  trclublem  14346  imasleval  16806  invsym2  17025  oppcsect2  17041  odupos  17737  oduposb  17738  oduglb  17741  odulub  17743  posglbd  17752  gsumcom3  19091  ordtbas2  21796  ordtcnv  21806  ordtrest2  21809  utop2nei  22856  utop3cls  22857  dvlt0  24608  dvcnvrelem1  24620  ofpreima  30428  funcnvmpt  30430  oduprs  30669  odutos  30676  tosglblem  30682  mcgcnv  30705  ordtcnvNEW  31273  ordtrest2NEW  31276  xrge0iifiso  31288  erdszelem9  32559  coepr  33101  dffr5  33102  dfso2  33103  cnvco1  33108  cnvco2  33109  pocnv  33112  nomaxmo  33314  txpss3v  33452  brtxp  33454  brpprod3b  33461  idsset  33464  fixcnv  33482  brimage  33500  brcup  33513  brcap  33514  dfrecs2  33524  dfrdg4  33525  dfint3  33526  imagesset  33527  brlb  33529  fvline  33718  ellines  33726  trer  33777  poimirlem31  35088  poimir  35090  frinfm  35173  xrnss3v  35784  rencldnfilem  39761  cnvssco  40306  psshepw  40489  dffrege115  40679  frege131  40695  frege133  40697  gte-lteh  45252  gt-lth  45253