Theorem brcnv 5780

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108  Vcvv 3422   class class class wbr 5070  ^◡ccnv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588

This theorem is referenced by:  cnvco  5783  dfrn2  5786  dfdm4  5793  cnvsym  6008  intasym  6009  asymref  6010  qfto  6015  dminss  6045  imainss  6046  dminxp  6072  cnvcnv3  6080  cnvpo  6179  cnvso  6180  dffun2  6428  funcnvsn  6468  funcnv2  6486  fun2cnv  6489  imadif  6502  f1ompt  6967  foeqcnvco  7152  f1eqcocnv  7153  f1eqcocnvOLD  7154  fliftcnv  7162  isocnv2  7182  fsplit  7928  fsplitOLD  7929  ercnv  8477  ecid  8529  omxpenlem  8813  sbthcl  8835  fimax2g  8990  dfsup2  9133  eqinf  9173  infval  9175  infcllem  9176  wofib  9234  oemapso  9370  cflim2  9950  fin23lem40  10038  isfin1-3  10073  fin12  10100  negiso  11885  dfinfre  11886  infrenegsup  11888  xrinfmss2  12974  trclublem  14634  imasleval  17169  invsym2  17392  oppcsect2  17408  odupos  17961  oduposb  17962  odulub  18040  oduglb  18042  posglbdg  18048  gsumcom3  19494  ordtbas2  22250  ordtcnv  22260  ordtrest2  22263  utop2nei  23310  utop3cls  23311  dvlt0  25074  dvcnvrelem1  25086  ofpreima  30904  funcnvmpt  30906  oduprs  31144  odutos  31148  tosglblem  31154  mgccnv  31179  ordtcnvNEW  31772  ordtrest2NEW  31775  xrge0iifiso  31787  erdszelem9  33061  coepr  33626  dffr5  33627  dfso2  33628  cnvco1  33632  cnvco2  33633  pocnv  33636  nomaxmo  33828  txpss3v  34107  brtxp  34109  brpprod3b  34116  idsset  34119  fixcnv  34137  brimage  34155  brcup  34168  brcap  34169  dfrecs2  34179  dfrdg4  34180  dfint3  34181  imagesset  34182  brlb  34184  fvline  34373  ellines  34381  trer  34432  poimirlem31  35735  poimir  35737  frinfm  35820  xrnss3v  36429  rencldnfilem  40558  cnvssco  41103  psshepw  41285  dffrege115  41475  frege131  41491  frege133  41493  gte-lteh  46314  gt-lth  46315