Theorem brcnv 5846

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3447   class class class wbr 5107  ^◡ccnv 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646

This theorem is referenced by:  cnvco  5849  dfrn2  5852  dfdm4  5859  cnvsym  6085  cnvsymOLD  6086  cnvsymOLDOLD  6087  intasym  6088  asymref  6089  qfto  6094  dminss  6126  imainss  6127  dminxp  6153  cnvcnv3  6161  cnvpo  6260  cnvso  6261  dffun2  6521  dffun2OLD  6522  dffun2OLDOLD  6523  funcnvsn  6566  funcnv2  6584  fun2cnv  6587  imadif  6600  f1ompt  7083  foeqcnvco  7275  f1eqcocnv  7276  fliftcnv  7286  isocnv2  7306  fsplit  8096  ercnv  8692  ecid  8753  omxpenlem  9042  sbthcl  9063  fimax2g  9233  dfsup2  9395  eqinf  9436  infval  9438  infcllem  9439  wofib  9498  oemapso  9635  cflim2  10216  fin23lem40  10304  isfin1-3  10339  fin12  10366  negiso  12163  dfinfre  12164  infrenegsup  12166  xrinfmss2  13271  trclublem  14961  imasleval  17504  invsym2  17725  oppcsect2  17741  oduprs  18261  odupos  18287  oduposb  18288  odulub  18366  oduglb  18368  posglbdg  18374  gsumcom3  19908  ordtbas2  23078  ordtcnv  23088  ordtrest2  23091  utop2nei  24138  utop3cls  24139  dvlt0  25910  dvcnvrelem1  25922  nomaxmo  27610  ofpreima  32589  funcnvmpt  32591  odutos  32894  tosglblem  32900  mgccnv  32925  ordtcnvNEW  33910  ordtrest2NEW  33913  xrge0iifiso  33925  erdszelem9  35186  coepr  35740  dffr5  35741  dfso2  35742  cnvco1  35746  cnvco2  35747  pocnv  35750  txpss3v  35866  brtxp  35868  brpprod3b  35875  idsset  35878  fixcnv  35896  brimage  35914  brcup  35927  brcap  35928  dfrecs2  35938  dfrdg4  35939  dfint3  35940  imagesset  35941  brlb  35943  fvline  36132  ellines  36140  trer  36304  poimirlem31  37645  poimir  37647  frinfm  37729  xrnss3v  38354  rencldnfilem  42808  cnvssco  43595  psshepw  43777  dffrege115  43967  frege131  43983  frege133  43985  brpermmodel  44993  lambert0  46888  lamberte  46889  gte-lteh  49715  gt-lth  49716