Theorem brcnv 5881

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   class class class wbr 5148  ^◡ccnv 5675

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684

This theorem is referenced by:  cnvco  5884  dfrn2  5887  dfdm4  5894  cnvsym  6111  cnvsymOLD  6112  cnvsymOLDOLD  6113  intasym  6114  asymref  6115  qfto  6120  dminss  6150  imainss  6151  dminxp  6177  cnvcnv3  6185  cnvpo  6284  cnvso  6285  dffun2  6551  dffun2OLD  6552  dffun2OLDOLD  6553  funcnvsn  6596  funcnv2  6614  fun2cnv  6617  imadif  6630  f1ompt  7108  foeqcnvco  7295  f1eqcocnv  7296  f1eqcocnvOLD  7297  fliftcnv  7305  isocnv2  7325  fsplit  8100  ercnv  8721  ecid  8773  omxpenlem  9070  sbthcl  9092  fimax2g  9286  dfsup2  9436  eqinf  9476  infval  9478  infcllem  9479  wofib  9537  oemapso  9674  cflim2  10255  fin23lem40  10343  isfin1-3  10378  fin12  10405  negiso  12191  dfinfre  12192  infrenegsup  12194  xrinfmss2  13287  trclublem  14939  imasleval  17484  invsym2  17707  oppcsect2  17723  odupos  18278  oduposb  18279  odulub  18357  oduglb  18359  posglbdg  18365  gsumcom3  19841  ordtbas2  22687  ordtcnv  22697  ordtrest2  22700  utop2nei  23747  utop3cls  23748  dvlt0  25514  dvcnvrelem1  25526  nomaxmo  27191  ofpreima  31878  funcnvmpt  31880  oduprs  32122  odutos  32126  tosglblem  32132  mgccnv  32157  ordtcnvNEW  32889  ordtrest2NEW  32892  xrge0iifiso  32904  erdszelem9  34179  coepr  34712  dffr5  34713  dfso2  34714  cnvco1  34718  cnvco2  34719  pocnv  34722  txpss3v  34839  brtxp  34841  brpprod3b  34848  idsset  34851  fixcnv  34869  brimage  34887  brcup  34900  brcap  34901  dfrecs2  34911  dfrdg4  34912  dfint3  34913  imagesset  34914  brlb  34916  fvline  35105  ellines  35113  trer  35190  poimirlem31  36508  poimir  36510  frinfm  36592  xrnss3v  37231  rencldnfilem  41544  cnvssco  42343  psshepw  42525  dffrege115  42715  frege131  42731  frege133  42733  gte-lteh  47725  gt-lth  47726