Theorem brcnv 5826

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

Syntax hints:   ↔ wb 208   ∈ wcel 2121  Vcvv 3433   class class class wbr 5074  ^◡ccnv 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  cnvco  5833  dfrn2  5836  dfdm4  5843  cnvsym  6070  intasym  6071  asymref  6072  qfto  6077  dminss  6107  imainss  6108  dminxp  6134  cnvcnv3  6142  cnvpo  6241  cnvso  6242  dffun2  6498  funcnvsn  6538  funcnv2  6556  fun2cnv  6559  imadif  6572  funcnvmpt  6940  f1ompt  7055  foeqcnvco  7247  f1eqcocnv  7248  fliftcnv  7258  isocnv2  7278  fsplit  8058  ercnv  8659  ecid  8721  omxpenlem  9010  sbthcl  9031  fimax2g  9190  dfsup2  9351  eqinf  9392  infval  9394  infcllem  9395  wofib  9454  oemapso  9598  cflim2  10181  fin23lem40  10269  isfin1-3  10304  fin12  10331  negiso  12131  dfinfre  12132  infrenegsup  12134  xrinfmss2  13258  trclublem  14952  imasleval  17500  invsym2  17725  oppcsect2  17741  oduprs  18261  odupos  18287  oduposb  18288  odulub  18366  oduglb  18368  posglbdg  18374  chnrev  18588  gsumcom3  19947  ordtbas2  23177  ordtcnv  23187  ordtrest2  23190  utop2nei  24236  utop3cls  24237  dvlt0  25993  dvcnvrelem1  26005  nomaxmo  27682  ofpreima  32759  odutos  33049  tosglblem  33055  mgccnv  33080  ordtcnvNEW  34114  ordtrest2NEW  34117  xrge0iifiso  34129  erdszelem9  35440  coepr  35994  dffr5  35995  dfso2  35996  cnvco1  36000  cnvco2  36001  pocnv  36004  txpss3v  36117  brtxp  36119  brpprod3b  36126  idsset  36129  fixcnv  36147  brimage  36165  brcup  36178  brcap  36179  dfrecs2  36191  dfrdg4  36192  dfint3  36193  imagesset  36194  brlb  36196  fvline  36385  ellines  36393  trer  36557  poimirlem31  38031  poimir  38033  frinfm  38115  xrnss3v  38761  rencldnfilem  43278  cnvssco  44063  psshepw  44245  dffrege115  44435  frege131  44451  frege133  44453  brpermmodel  45460  lambert0  47362  lamberte  47363  gte-lteh  50228  gt-lth  50229