Theorem brcnv 5849

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110  ^◡ccnv 5640

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-cnv 5649

This theorem is referenced by:  cnvco  5852  dfrn2  5855  dfdm4  5862  cnvsym  6088  cnvsymOLD  6089  cnvsymOLDOLD  6090  intasym  6091  asymref  6092  qfto  6097  dminss  6129  imainss  6130  dminxp  6156  cnvcnv3  6164  cnvpo  6263  cnvso  6264  dffun2  6524  dffun2OLD  6525  dffun2OLDOLD  6526  funcnvsn  6569  funcnv2  6587  fun2cnv  6590  imadif  6603  f1ompt  7086  foeqcnvco  7278  f1eqcocnv  7279  fliftcnv  7289  isocnv2  7309  fsplit  8099  ercnv  8695  ecid  8756  omxpenlem  9047  sbthcl  9069  fimax2g  9240  dfsup2  9402  eqinf  9443  infval  9445  infcllem  9446  wofib  9505  oemapso  9642  cflim2  10223  fin23lem40  10311  isfin1-3  10346  fin12  10373  negiso  12170  dfinfre  12171  infrenegsup  12173  xrinfmss2  13278  trclublem  14968  imasleval  17511  invsym2  17732  oppcsect2  17748  oduprs  18268  odupos  18294  oduposb  18295  odulub  18373  oduglb  18375  posglbdg  18381  gsumcom3  19915  ordtbas2  23085  ordtcnv  23095  ordtrest2  23098  utop2nei  24145  utop3cls  24146  dvlt0  25917  dvcnvrelem1  25929  nomaxmo  27617  ofpreima  32596  funcnvmpt  32598  odutos  32901  tosglblem  32907  mgccnv  32932  ordtcnvNEW  33917  ordtrest2NEW  33920  xrge0iifiso  33932  erdszelem9  35193  coepr  35747  dffr5  35748  dfso2  35749  cnvco1  35753  cnvco2  35754  pocnv  35757  txpss3v  35873  brtxp  35875  brpprod3b  35882  idsset  35885  fixcnv  35903  brimage  35921  brcup  35934  brcap  35935  dfrecs2  35945  dfrdg4  35946  dfint3  35947  imagesset  35948  brlb  35950  fvline  36139  ellines  36147  trer  36311  poimirlem31  37652  poimir  37654  frinfm  37736  xrnss3v  38361  rencldnfilem  42815  cnvssco  43602  psshepw  43784  dffrege115  43974  frege131  43990  frege133  43992  brpermmodel  45000  lambert0  46895  lamberte  46896  gte-lteh  49719  gt-lth  49720