Theorem brcnv 5190

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
opelcnv.2

Assertion

Ref	Expression
brcnv

Proof of Theorem brcnv

Step	Hyp	Ref	Expression
1		opelcnv.1	. 2
2		opelcnv.2	. 2
3		brcnvg 5188	. 2
4	1, 2, 3	mp2an 672	1

Syntax hints:  <->wb 184  e.wcel 1818  cvv 3109   class class class wbr 4452  `'ccnv 5003

This theorem is referenced by:  cnvco  5193  dfrn2  5196  dfdm4  5200  cnvsym  5386  intasym  5387  asymref  5388  qfto  5393  dminss  5425  imainss  5426  dminxp  5452  cnvcnv3  5461  cnvpo  5550  cnvso  5551  dffun2  5603  funcnvsn  5638  funcnv2  5652  fun2cnv  5655  imadif  5668  f1ompt  6053  foeqcnvco  6203  f1eqcocnv  6204  fliftcnv  6209  isocnv2  6227  fsplit  6905  ercnv  7351  ecid  7395  omxpenlem  7638  sbthcl  7659  fimax2g  7786  dfsup2  7922  dfsup2OLD  7923  wofib  7991  oemapso  8122  cflim2  8664  fin23lem40  8752  isfin1-3  8787  fin12  8814  negiso  10544  dfinfmr  10545  infmsup  10546  infmrgelb  10548  infmrlb  10549  xrinfmss2  11531  xrinfm0  11557  ramcl2lem  14527  imasleval  14938  invsym2  15157  oppcsect2  15169  odupos  15765  oduposb  15766  oduglb  15769  odulub  15771  posglbd  15780  gsumcom3  18901  ordtbas2  19692  ordtcnv  19702  ordtrest2  19705  utop2nei  20753  utop3cls  20754  dvlt0  22406  dvcnvrelem1  22418  ofpreima  27507  funcnvmptOLD  27509  funcnvmpt  27510  xrge0infss  27580  oduprs  27644  odutos  27651  tosglblem  27657  ordtcnvNEW  27902  ordtrest2NEW  27905  xrge0iifiso  27917  ballotlemfrcn0  28468  erdszelem9  28643  coepr  29181  dffr5  29182  dfso2  29183  cnvco1  29189  cnvco2  29190  pocnv  29193  socnv  29194  wzel  29380  wsuclem  29381  txpss3v  29528  brtxp  29530  brpprod3b  29537  idsset  29540  fixcnv  29558  brimage  29576  brcup  29589  brcap  29590  dfrdg4  29600  tfrqfree  29601  dfint3  29602  imagesset  29603  brlb  29605  fvline  29794  ellines  29802  trer  30134  gtinf  30137  frinfm  30226  rencldnfilem  30754  lcmgcdlem  31212  infrglb  31584  gte-lteh  33120  gt-lth  33121  trclubg  37785  psshepw  37811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-cnv 5012