Theorem brcnv 5821

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  Vcvv 3436   class class class wbr 5089  ^◡ccnv 5613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-cnv 5622

This theorem is referenced by:  cnvco  5824  dfrn2  5827  dfdm4  5834  cnvsym  6060  intasym  6061  asymref  6062  qfto  6067  dminss  6100  imainss  6101  dminxp  6127  cnvcnv3  6135  cnvpo  6234  cnvso  6235  dffun2  6491  funcnvsn  6531  funcnv2  6549  fun2cnv  6552  imadif  6565  f1ompt  7044  foeqcnvco  7234  f1eqcocnv  7235  fliftcnv  7245  isocnv2  7265  fsplit  8047  ercnv  8643  ecid  8704  omxpenlem  8991  sbthcl  9012  fimax2g  9170  dfsup2  9328  eqinf  9369  infval  9371  infcllem  9372  wofib  9431  oemapso  9572  cflim2  10154  fin23lem40  10242  isfin1-3  10277  fin12  10304  negiso  12102  dfinfre  12103  infrenegsup  12105  xrinfmss2  13210  trclublem  14902  imasleval  17445  invsym2  17670  oppcsect2  17686  oduprs  18206  odupos  18232  oduposb  18233  odulub  18311  oduglb  18313  posglbdg  18319  chnrev  18533  gsumcom3  19890  ordtbas2  23106  ordtcnv  23116  ordtrest2  23119  utop2nei  24165  utop3cls  24166  dvlt0  25937  dvcnvrelem1  25949  nomaxmo  27637  ofpreima  32647  funcnvmpt  32649  odutos  32949  tosglblem  32955  mgccnv  32980  ordtcnvNEW  33933  ordtrest2NEW  33936  xrge0iifiso  33948  erdszelem9  35243  coepr  35797  dffr5  35798  dfso2  35799  cnvco1  35803  cnvco2  35804  pocnv  35807  txpss3v  35920  brtxp  35922  brpprod3b  35929  idsset  35932  fixcnv  35950  brimage  35968  brcup  35981  brcap  35982  dfrecs2  35994  dfrdg4  35995  dfint3  35996  imagesset  35997  brlb  35999  fvline  36188  ellines  36196  trer  36360  poimirlem31  37690  poimir  37692  frinfm  37774  xrnss3v  38404  rencldnfilem  42912  cnvssco  43698  psshepw  43880  dffrege115  44070  frege131  44086  frege133  44088  brpermmodel  45095  lambert0  46986  lamberte  46987  gte-lteh  49826  gt-lth  49827