Theorem brcnv 5893

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3480   class class class wbr 5143  ^◡ccnv 5684

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-cnv 5693

This theorem is referenced by:  cnvco  5896  dfrn2  5899  dfdm4  5906  cnvsym  6132  cnvsymOLD  6133  cnvsymOLDOLD  6134  intasym  6135  asymref  6136  qfto  6141  dminss  6173  imainss  6174  dminxp  6200  cnvcnv3  6208  cnvpo  6307  cnvso  6308  dffun2  6571  dffun2OLD  6572  dffun2OLDOLD  6573  funcnvsn  6616  funcnv2  6634  fun2cnv  6637  imadif  6650  f1ompt  7131  foeqcnvco  7320  f1eqcocnv  7321  fliftcnv  7331  isocnv2  7351  fsplit  8142  ercnv  8766  ecid  8822  omxpenlem  9113  sbthcl  9135  fimax2g  9322  dfsup2  9484  eqinf  9524  infval  9526  infcllem  9527  wofib  9585  oemapso  9722  cflim2  10303  fin23lem40  10391  isfin1-3  10426  fin12  10453  negiso  12248  dfinfre  12249  infrenegsup  12251  xrinfmss2  13353  trclublem  15034  imasleval  17586  invsym2  17807  oppcsect2  17823  oduprs  18346  odupos  18373  oduposb  18374  odulub  18452  oduglb  18454  posglbdg  18460  gsumcom3  19996  ordtbas2  23199  ordtcnv  23209  ordtrest2  23212  utop2nei  24259  utop3cls  24260  dvlt0  26044  dvcnvrelem1  26056  nomaxmo  27743  ofpreima  32675  funcnvmpt  32677  odutos  32958  tosglblem  32964  mgccnv  32989  ordtcnvNEW  33919  ordtrest2NEW  33922  xrge0iifiso  33934  erdszelem9  35204  coepr  35753  dffr5  35754  dfso2  35755  cnvco1  35759  cnvco2  35760  pocnv  35763  txpss3v  35879  brtxp  35881  brpprod3b  35888  idsset  35891  fixcnv  35909  brimage  35927  brcup  35940  brcap  35941  dfrecs2  35951  dfrdg4  35952  dfint3  35953  imagesset  35954  brlb  35956  fvline  36145  ellines  36153  trer  36317  poimirlem31  37658  poimir  37660  frinfm  37742  xrnss3v  38373  rencldnfilem  42831  cnvssco  43619  psshepw  43801  dffrege115  43991  frege131  44007  frege133  44009  gte-lteh  49245  gt-lth  49246