Theorem brcnv 5830

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3439   class class class wbr 5097  ^◡ccnv 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-cnv 5631

This theorem is referenced by:  cnvco  5833  dfrn2  5836  dfdm4  5843  cnvsym  6070  intasym  6071  asymref  6072  qfto  6077  dminss  6110  imainss  6111  dminxp  6137  cnvcnv3  6145  cnvpo  6244  cnvso  6245  dffun2  6501  funcnvsn  6541  funcnv2  6559  fun2cnv  6562  imadif  6575  funcnvmpt  6942  f1ompt  7056  foeqcnvco  7246  f1eqcocnv  7247  fliftcnv  7257  isocnv2  7277  fsplit  8059  ercnv  8657  ecid  8719  omxpenlem  9008  sbthcl  9029  fimax2g  9188  dfsup2  9349  eqinf  9390  infval  9392  infcllem  9393  wofib  9452  oemapso  9593  cflim2  10175  fin23lem40  10263  isfin1-3  10298  fin12  10325  negiso  12124  dfinfre  12125  infrenegsup  12127  xrinfmss2  13228  trclublem  14920  imasleval  17464  invsym2  17689  oppcsect2  17705  oduprs  18225  odupos  18251  oduposb  18252  odulub  18330  oduglb  18332  posglbdg  18338  chnrev  18552  gsumcom3  19909  ordtbas2  23137  ordtcnv  23147  ordtrest2  23150  utop2nei  24196  utop3cls  24197  dvlt0  25968  dvcnvrelem1  25980  nomaxmo  27668  ofpreima  32723  odutos  33029  tosglblem  33035  mgccnv  33060  ordtcnvNEW  34056  ordtrest2NEW  34059  xrge0iifiso  34071  erdszelem9  35372  coepr  35926  dffr5  35927  dfso2  35928  cnvco1  35932  cnvco2  35933  pocnv  35936  txpss3v  36049  brtxp  36051  brpprod3b  36058  idsset  36061  fixcnv  36079  brimage  36097  brcup  36110  brcap  36111  dfrecs2  36123  dfrdg4  36124  dfint3  36125  imagesset  36126  brlb  36128  fvline  36317  ellines  36325  trer  36489  poimirlem31  37821  poimir  37823  frinfm  37905  xrnss3v  38551  rencldnfilem  43099  cnvssco  43884  psshepw  44066  dffrege115  44256  frege131  44272  frege133  44274  brpermmodel  45281  lambert0  47170  lamberte  47171  gte-lteh  50008  gt-lth  50009