Theorem brcnv 5859

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102  ^◡ccnv 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-cnv 5658

This theorem is used by:  cnvco  5866  dfrn2  5869  dfdm4  5876  cnvsym  6107  intasym  6108  asymref  6109  qfto  6114  dminss  6142  imainss  6143  cnvxp  6146  xpdifcnvepel  6159  dminxp  6171  cnvcnv3  6179  cnvpo  6290  cnvso  6291  dffun2  6548  funcnvsn  6590  funcnv2  6608  fun2cnv  6611  imadif  6624  funcnvmpt  6995  f1ompt  7111  foeqcnvco  7308  f1eqcocnv  7309  fliftcnv  7319  isocnv2  7339  fsplit  8128  ercnv  8739  ecid  8801  omxpenlem  9097  sbthcl  9118  fimax2g  9277  dfsup2  9436  eqinf  9477  infval  9479  infcllem  9480  wofib  9539  oemapso  9683  cflim2  10341  fin23lem40  10429  isfin1-3  10464  fin12  10491  negiso  12297  dfinfre  12298  infrenegsup  12300  xrinfmss2  13441  trclublem  15148  imasleval  17713  invsym2  17938  oppcsect2  17954  oduprs  18474  odupos  18500  oduposb  18501  odulub  18579  oduglb  18581  posglbdg  18587  chnrev  18801  gsumcom3  20192  ordtbas2  23509  ordtcnv  23519  ordtrest2  23522  utop2nei  24569  utop3cls  24570  dvlt0  26325  dvcnvrelem1  26337  nomaxmo  28055  ofpreima  33259  odutos  33529  tosglblem  33535  mgccnv  33560  ordtcnvNEW  34552  ordtrest2NEW  34555  xrge0iifiso  34567  erdszelem9  35964  coepr  36518  dffr5  36519  dfso2  36520  cnvco1  36524  cnvco2  36525  pocnv  36528  txpss3v  36640  brtxp  36642  brpprod3b  36649  idsset  36652  fixcnv  36670  brimage  36688  brcup  36701  brcap  36702  dfrecs2  36714  dfrdg4  36715  dfint3  36716  imagesset  36717  brlb  36719  fvline  36909  ellines  36917  trer  37104  poimirlem31  38570  poimir  38572  frinfm  38670  xrnss3v  39314  rencldnfilem  43827  cnvssco  44606  psshepw  44788  dffrege115  44978  frege131  44994  frege133  44996  brpermmodel  45993  lambert0  47937  lamberte  47938  gte-lteh  50819  gt-lth  50820