Theorem brcnv 5856

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

Syntax hints:   ↔ wb 208   ∈ wcel 2144  Vcvv 3456   class class class wbr 5102  ^◡ccnv 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-cnv 5657

This theorem is referenced by:  cnvco  5863  dfrn2  5866  dfdm4  5873  cnvsym  6103  intasym  6104  asymref  6105  qfto  6110  dminss  6140  imainss  6141  xpdifcnvepel  6156  dminxp  6168  cnvcnv3  6176  cnvpo  6276  cnvso  6277  dffun2  6533  funcnvsn  6573  funcnv2  6591  fun2cnv  6594  imadif  6607  funcnvmpt  6979  f1ompt  7094  foeqcnvco  7286  f1eqcocnv  7287  fliftcnv  7297  isocnv2  7317  fsplit  8098  ercnv  8702  ecid  8764  omxpenlem  9052  sbthcl  9073  fimax2g  9232  dfsup2  9392  eqinf  9433  infval  9435  infcllem  9436  wofib  9495  oemapso  9639  cflim2  10222  fin23lem40  10310  isfin1-3  10345  fin12  10372  negiso  12174  dfinfre  12175  infrenegsup  12177  xrinfmss2  13316  trclublem  15010  imasleval  17573  invsym2  17798  oppcsect2  17814  oduprs  18334  odupos  18360  oduposb  18361  odulub  18439  oduglb  18441  posglbdg  18447  chnrev  18661  gsumcom3  20020  ordtbas2  23253  ordtcnv  23263  ordtrest2  23266  utop2nei  24312  utop3cls  24313  dvlt0  26069  dvcnvrelem1  26081  nomaxmo  27764  ofpreima  32869  odutos  33148  tosglblem  33154  mgccnv  33179  ordtcnvNEW  34219  ordtrest2NEW  34222  xrge0iifiso  34234  erdszelem9  35554  coepr  36108  dffr5  36109  dfso2  36110  cnvco1  36114  cnvco2  36115  pocnv  36118  txpss3v  36231  brtxp  36233  brpprod3b  36240  idsset  36243  fixcnv  36261  brimage  36279  brcup  36292  brcap  36293  dfrecs2  36305  dfrdg4  36306  dfint3  36307  imagesset  36308  brlb  36310  fvline  36499  ellines  36507  trer  36681  poimirlem31  38155  poimir  38157  frinfm  38239  xrnss3v  38885  rencldnfilem  43402  cnvssco  44187  psshepw  44369  dffrege115  44559  frege131  44575  frege133  44577  brpermmodel  45584  lambert0  47486  lamberte  47487  gte-lteh  50352  gt-lth  50353