Theorem brcnv 5869

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

Syntax hints:   ↔ wb 209   ∈ wcel 2149  Vcvv 3461   class class class wbr 5111  ^◡ccnv 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112  df-opab 5176  df-cnv 5670

This theorem is referenced by:  cnvco  5876  dfrn2  5879  dfdm4  5886  cnvsym  6115  intasym  6116  asymref  6117  qfto  6122  dminss  6151  imainss  6152  xpdifcnvepel  6167  dminxp  6179  cnvcnv3  6187  cnvpo  6289  cnvso  6290  dffun2  6547  funcnvsn  6587  funcnv2  6605  fun2cnv  6608  imadif  6621  funcnvmpt  6992  f1ompt  7107  foeqcnvco  7299  f1eqcocnv  7300  fliftcnv  7310  isocnv2  7330  fsplit  8112  ercnv  8716  ecid  8778  omxpenlem  9066  sbthcl  9087  fimax2g  9246  dfsup2  9404  eqinf  9445  infval  9447  infcllem  9448  wofib  9507  oemapso  9651  cflim2  10247  fin23lem40  10335  isfin1-3  10370  fin12  10397  negiso  12195  dfinfre  12196  infrenegsup  12198  xrinfmss2  13337  trclublem  15032  imasleval  17595  invsym2  17820  oppcsect2  17836  oduprs  18356  odupos  18382  oduposb  18383  odulub  18461  oduglb  18463  posglbdg  18469  chnrev  18683  gsumcom3  20048  ordtbas2  23317  ordtcnv  23327  ordtrest2  23330  utop2nei  24376  utop3cls  24377  dvlt0  26133  dvcnvrelem1  26145  nomaxmo  27828  ofpreima  32951  odutos  33229  tosglblem  33235  mgccnv  33260  ordtcnvNEW  34255  ordtrest2NEW  34258  xrge0iifiso  34270  erdszelem9  35624  coepr  36178  dffr5  36179  dfso2  36180  cnvco1  36184  cnvco2  36185  pocnv  36188  txpss3v  36301  brtxp  36303  brpprod3b  36310  idsset  36313  fixcnv  36331  brimage  36349  brcup  36362  brcap  36363  dfrecs2  36375  dfrdg4  36376  dfint3  36377  imagesset  36378  brlb  36380  fvline  36569  ellines  36577  trer  36750  poimirlem31  38225  poimir  38227  frinfm  38309  xrnss3v  38955  rencldnfilem  43474  cnvssco  44259  psshepw  44441  dffrege115  44631  frege131  44647  frege133  44649  brpermmodel  45639  lambert0  47548  lamberte  47549  gte-lteh  50424  gt-lth  50425