Theorem brcnv 5880

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

Syntax hints:   ↔ wb 205   ∈ wcel 2099  Vcvv 3470   class class class wbr 5143  ^◡ccnv 5672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144  df-opab 5206  df-cnv 5681

This theorem is referenced by:  cnvco  5883  dfrn2  5886  dfdm4  5893  cnvsym  6113  cnvsymOLD  6114  cnvsymOLDOLD  6115  intasym  6116  asymref  6117  qfto  6122  dminss  6152  imainss  6153  dminxp  6179  cnvcnv3  6187  cnvpo  6286  cnvso  6287  dffun2  6553  dffun2OLD  6554  dffun2OLDOLD  6555  funcnvsn  6598  funcnv2  6616  fun2cnv  6619  imadif  6632  f1ompt  7116  foeqcnvco  7304  f1eqcocnv  7305  f1eqcocnvOLD  7306  fliftcnv  7314  isocnv2  7334  fsplit  8117  ercnv  8740  ecid  8795  omxpenlem  9092  sbthcl  9114  fimax2g  9308  dfsup2  9462  eqinf  9502  infval  9504  infcllem  9505  wofib  9563  oemapso  9700  cflim2  10281  fin23lem40  10369  isfin1-3  10404  fin12  10431  negiso  12219  dfinfre  12220  infrenegsup  12222  xrinfmss2  13317  trclublem  14969  imasleval  17517  invsym2  17740  oppcsect2  17756  odupos  18314  oduposb  18315  odulub  18393  oduglb  18395  posglbdg  18401  gsumcom3  19927  ordtbas2  23089  ordtcnv  23099  ordtrest2  23102  utop2nei  24149  utop3cls  24150  dvlt0  25932  dvcnvrelem1  25944  nomaxmo  27625  ofpreima  32445  funcnvmpt  32447  oduprs  32686  odutos  32690  tosglblem  32696  mgccnv  32721  ordtcnvNEW  33516  ordtrest2NEW  33519  xrge0iifiso  33531  erdszelem9  34804  coepr  35342  dffr5  35343  dfso2  35344  cnvco1  35348  cnvco2  35349  pocnv  35352  txpss3v  35469  brtxp  35471  brpprod3b  35478  idsset  35481  fixcnv  35499  brimage  35517  brcup  35530  brcap  35531  dfrecs2  35541  dfrdg4  35542  dfint3  35543  imagesset  35544  brlb  35546  fvline  35735  ellines  35743  trer  35795  poimirlem31  37119  poimir  37121  frinfm  37203  xrnss3v  37839  rencldnfilem  42231  cnvssco  43027  psshepw  43209  dffrege115  43399  frege131  43415  frege133  43417  gte-lteh  48148  gt-lth  48149

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »