Theorem brcnv 5835

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3430   class class class wbr 5086  ^◡ccnv 5627

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5636

This theorem is referenced by:  cnvco  5838  dfrn2  5841  dfdm4  5848  cnvsym  6075  intasym  6076  asymref  6077  qfto  6082  dminss  6115  imainss  6116  dminxp  6142  cnvcnv3  6150  cnvpo  6249  cnvso  6250  dffun2  6506  funcnvsn  6546  funcnv2  6564  fun2cnv  6567  imadif  6580  funcnvmpt  6947  f1ompt  7061  foeqcnvco  7252  f1eqcocnv  7253  fliftcnv  7263  isocnv2  7283  fsplit  8064  ercnv  8662  ecid  8724  omxpenlem  9013  sbthcl  9034  fimax2g  9193  dfsup2  9354  eqinf  9395  infval  9397  infcllem  9398  wofib  9457  oemapso  9600  cflim2  10182  fin23lem40  10270  isfin1-3  10305  fin12  10332  negiso  12133  dfinfre  12134  infrenegsup  12136  xrinfmss2  13260  trclublem  14954  imasleval  17502  invsym2  17727  oppcsect2  17743  oduprs  18263  odupos  18289  oduposb  18290  odulub  18368  oduglb  18370  posglbdg  18376  chnrev  18590  gsumcom3  19950  ordtbas2  23172  ordtcnv  23182  ordtrest2  23185  utop2nei  24231  utop3cls  24232  dvlt0  25988  dvcnvrelem1  26000  nomaxmo  27682  ofpreima  32759  odutos  33049  tosglblem  33055  mgccnv  33080  ordtcnvNEW  34086  ordtrest2NEW  34089  xrge0iifiso  34101  erdszelem9  35403  coepr  35957  dffr5  35958  dfso2  35959  cnvco1  35963  cnvco2  35964  pocnv  35967  txpss3v  36080  brtxp  36082  brpprod3b  36089  idsset  36092  fixcnv  36110  brimage  36128  brcup  36141  brcap  36142  dfrecs2  36154  dfrdg4  36155  dfint3  36156  imagesset  36157  brlb  36159  fvline  36348  ellines  36356  trer  36520  poimirlem31  37994  poimir  37996  frinfm  38078  xrnss3v  38724  rencldnfilem  43274  cnvssco  44059  psshepw  44241  dffrege115  44431  frege131  44447  frege133  44449  brpermmodel  45456  lambert0  47355  lamberte  47356  gte-lteh  50221  gt-lth  50222