Theorem brcnv 5791

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

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

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 5223  ax-nul 5230  ax-pr 5352

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 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-cnv 5597

This theorem is referenced by:  cnvco  5794  dfrn2  5797  dfdm4  5804  cnvsym  6019  intasym  6020  asymref  6021  qfto  6026  dminss  6056  imainss  6057  dminxp  6083  cnvcnv3  6091  cnvpo  6190  cnvso  6191  dffun2  6443  dffun2OLD  6444  funcnvsn  6484  funcnv2  6502  fun2cnv  6505  imadif  6518  f1ompt  6985  foeqcnvco  7172  f1eqcocnv  7173  f1eqcocnvOLD  7174  fliftcnv  7182  isocnv2  7202  fsplit  7957  fsplitOLD  7958  ercnv  8519  ecid  8571  omxpenlem  8860  sbthcl  8882  fimax2g  9060  dfsup2  9203  eqinf  9243  infval  9245  infcllem  9246  wofib  9304  oemapso  9440  cflim2  10019  fin23lem40  10107  isfin1-3  10142  fin12  10169  negiso  11955  dfinfre  11956  infrenegsup  11958  xrinfmss2  13045  trclublem  14706  imasleval  17252  invsym2  17475  oppcsect2  17491  odupos  18046  oduposb  18047  odulub  18125  oduglb  18127  posglbdg  18133  gsumcom3  19579  ordtbas2  22342  ordtcnv  22352  ordtrest2  22355  utop2nei  23402  utop3cls  23403  dvlt0  25169  dvcnvrelem1  25181  ofpreima  31002  funcnvmpt  31004  oduprs  31242  odutos  31246  tosglblem  31252  mgccnv  31277  ordtcnvNEW  31870  ordtrest2NEW  31873  xrge0iifiso  31885  erdszelem9  33161  coepr  33720  dffr5  33721  dfso2  33722  cnvco1  33726  cnvco2  33727  pocnv  33730  nomaxmo  33901  txpss3v  34180  brtxp  34182  brpprod3b  34189  idsset  34192  fixcnv  34210  brimage  34228  brcup  34241  brcap  34242  dfrecs2  34252  dfrdg4  34253  dfint3  34254  imagesset  34255  brlb  34257  fvline  34446  ellines  34454  trer  34505  poimirlem31  35808  poimir  35810  frinfm  35893  xrnss3v  36502  rencldnfilem  40642  cnvssco  41214  psshepw  41396  dffrege115  41586  frege131  41602  frege133  41604  gte-lteh  46428  gt-lth  46429