Theorem brcnv 5889

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

Syntax hints:   ↔ wb 205   ∈ wcel 2099  Vcvv 3462   class class class wbr 5153  ^◡ccnv 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216  df-cnv 5690

This theorem is referenced by:  cnvco  5892  dfrn2  5895  dfdm4  5902  cnvsym  6124  cnvsymOLD  6125  cnvsymOLDOLD  6126  intasym  6127  asymref  6128  qfto  6133  dminss  6164  imainss  6165  dminxp  6191  cnvcnv3  6199  cnvpo  6298  cnvso  6299  dffun2  6564  dffun2OLD  6565  dffun2OLDOLD  6566  funcnvsn  6609  funcnv2  6627  fun2cnv  6630  imadif  6643  f1ompt  7125  foeqcnvco  7314  f1eqcocnv  7315  fliftcnv  7323  isocnv2  7343  fsplit  8131  ercnv  8755  ecid  8811  omxpenlem  9111  sbthcl  9133  fimax2g  9323  dfsup2  9487  eqinf  9527  infval  9529  infcllem  9530  wofib  9588  oemapso  9725  cflim2  10306  fin23lem40  10394  isfin1-3  10429  fin12  10456  negiso  12246  dfinfre  12247  infrenegsup  12249  xrinfmss2  13344  trclublem  15000  imasleval  17556  invsym2  17779  oppcsect2  17795  odupos  18353  oduposb  18354  odulub  18432  oduglb  18434  posglbdg  18440  gsumcom3  19976  ordtbas2  23186  ordtcnv  23196  ordtrest2  23199  utop2nei  24246  utop3cls  24247  dvlt0  26029  dvcnvrelem1  26041  nomaxmo  27728  ofpreima  32582  funcnvmpt  32584  oduprs  32834  odutos  32838  tosglblem  32844  mgccnv  32869  ordtcnvNEW  33735  ordtrest2NEW  33738  xrge0iifiso  33750  erdszelem9  35027  coepr  35575  dffr5  35576  dfso2  35577  cnvco1  35581  cnvco2  35582  pocnv  35585  txpss3v  35702  brtxp  35704  brpprod3b  35711  idsset  35714  fixcnv  35732  brimage  35750  brcup  35763  brcap  35764  dfrecs2  35774  dfrdg4  35775  dfint3  35776  imagesset  35777  brlb  35779  fvline  35968  ellines  35976  trer  36028  poimirlem31  37352  poimir  37354  frinfm  37436  xrnss3v  38070  rencldnfilem  42477  cnvssco  43273  psshepw  43455  dffrege115  43645  frege131  43661  frege133  43663  gte-lteh  48472  gt-lth  48473