Theorem brcnv 5552

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

Syntax hints:   ↔ wb 198   ∈ wcel 2107  Vcvv 3398   class class class wbr 4888  ^◡ccnv 5356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889  df-opab 4951  df-cnv 5365

This theorem is referenced by:  cnvco  5555  dfrn2  5558  dfdm4  5563  cnvsym  5767  intasym  5768  asymref  5769  qfto  5774  dminss  5803  imainss  5804  dminxp  5830  cnvcnv3  5838  cnvpo  5929  cnvso  5930  dffun2  6147  funcnvsn  6186  funcnv2  6204  fun2cnv  6207  imadif  6220  f1ompt  6647  foeqcnvco  6829  f1eqcocnv  6830  fliftcnv  6835  isocnv2  6855  fsplit  7565  ercnv  8049  ecid  8097  omxpenlem  8351  sbthcl  8372  fimax2g  8496  dfsup2  8640  eqinf  8680  infval  8682  infcllem  8683  wofib  8741  oemapso  8878  cflim2  9422  fin23lem40  9510  isfin1-3  9545  fin12  9572  negiso  11361  dfinfre  11362  infrenegsup  11364  xrinfmss2  12457  trclublem  14147  imasleval  16591  invsym2  16812  oppcsect2  16828  odupos  17525  oduposb  17526  oduglb  17529  odulub  17531  posglbd  17540  gsumcom3  20613  ordtbas2  21407  ordtcnv  21417  ordtrest2  21420  utop2nei  22466  utop3cls  22467  dvlt0  24209  dvcnvrelem1  24221  ofpreima  30034  funcnvmpt  30036  oduprs  30222  odutos  30229  tosglblem  30235  ordtcnvNEW  30568  ordtrest2NEW  30571  xrge0iifiso  30583  erdszelem9  31784  coepr  32240  dffr5  32241  dfso2  32242  cnvco1  32247  cnvco2  32248  pocnv  32251  nomaxmo  32440  txpss3v  32578  brtxp  32580  brpprod3b  32587  idsset  32590  fixcnv  32608  brimage  32626  brcup  32639  brcap  32640  dfrecs2  32650  dfrdg4  32651  dfint3  32652  imagesset  32653  brlb  32655  fvline  32844  ellines  32852  trer  32903  poimirlem31  34071  poimir  34073  frinfm  34160  xrnss3v  34767  rencldnfilem  38354  cnvssco  38879  psshepw  39048  dffrege115  39238  frege131  39254  frege133  39256  gte-lteh  43585  gt-lth  43586