Theorem brcnv 5825

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3436   class class class wbr 5092  ^◡ccnv 5618

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-cnv 5627

This theorem is referenced by:  cnvco  5828  dfrn2  5831  dfdm4  5838  cnvsym  6063  intasym  6064  asymref  6065  qfto  6070  dminss  6102  imainss  6103  dminxp  6129  cnvcnv3  6137  cnvpo  6235  cnvso  6236  dffun2  6492  funcnvsn  6532  funcnv2  6550  fun2cnv  6553  imadif  6566  f1ompt  7045  foeqcnvco  7237  f1eqcocnv  7238  fliftcnv  7248  isocnv2  7268  fsplit  8050  ercnv  8646  ecid  8707  omxpenlem  8995  sbthcl  9016  fimax2g  9175  dfsup2  9334  eqinf  9375  infval  9377  infcllem  9378  wofib  9437  oemapso  9578  cflim2  10157  fin23lem40  10245  isfin1-3  10280  fin12  10307  negiso  12105  dfinfre  12106  infrenegsup  12108  xrinfmss2  13213  trclublem  14902  imasleval  17445  invsym2  17670  oppcsect2  17686  oduprs  18206  odupos  18232  oduposb  18233  odulub  18311  oduglb  18313  posglbdg  18319  gsumcom3  19857  ordtbas2  23076  ordtcnv  23086  ordtrest2  23089  utop2nei  24136  utop3cls  24137  dvlt0  25908  dvcnvrelem1  25920  nomaxmo  27608  ofpreima  32616  funcnvmpt  32618  odutos  32919  tosglblem  32925  mgccnv  32950  ordtcnvNEW  33903  ordtrest2NEW  33906  xrge0iifiso  33918  erdszelem9  35192  coepr  35746  dffr5  35747  dfso2  35748  cnvco1  35752  cnvco2  35753  pocnv  35756  txpss3v  35872  brtxp  35874  brpprod3b  35881  idsset  35884  fixcnv  35902  brimage  35920  brcup  35933  brcap  35934  dfrecs2  35944  dfrdg4  35945  dfint3  35946  imagesset  35947  brlb  35949  fvline  36138  ellines  36146  trer  36310  poimirlem31  37651  poimir  37653  frinfm  37735  xrnss3v  38360  rencldnfilem  42813  cnvssco  43599  psshepw  43781  dffrege115  43971  frege131  43987  frege133  43989  brpermmodel  44997  lambert0  46891  lamberte  46892  gte-lteh  49731  gt-lth  49732