Theorem brcnv 5837

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3444   class class class wbr 5102  ^◡ccnv 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  cnvco  5840  dfrn2  5843  dfdm4  5850  cnvsym  6074  cnvsymOLD  6075  cnvsymOLDOLD  6076  intasym  6077  asymref  6078  qfto  6083  dminss  6115  imainss  6116  dminxp  6142  cnvcnv3  6150  cnvpo  6249  cnvso  6250  dffun2  6510  dffun2OLD  6511  funcnvsn  6551  funcnv2  6569  fun2cnv  6572  imadif  6585  f1ompt  7066  foeqcnvco  7258  f1eqcocnv  7259  fliftcnv  7269  isocnv2  7289  fsplit  8074  ercnv  8670  ecid  8731  omxpenlem  9020  sbthcl  9041  fimax2g  9210  dfsup2  9372  eqinf  9413  infval  9415  infcllem  9416  wofib  9475  oemapso  9614  cflim2  10195  fin23lem40  10283  isfin1-3  10318  fin12  10345  negiso  12142  dfinfre  12143  infrenegsup  12145  xrinfmss2  13250  trclublem  14939  imasleval  17482  invsym2  17707  oppcsect2  17723  oduprs  18243  odupos  18269  oduposb  18270  odulub  18348  oduglb  18350  posglbdg  18356  gsumcom3  19894  ordtbas2  23113  ordtcnv  23123  ordtrest2  23126  utop2nei  24173  utop3cls  24174  dvlt0  25945  dvcnvrelem1  25957  nomaxmo  27645  ofpreima  32641  funcnvmpt  32643  odutos  32942  tosglblem  32948  mgccnv  32973  ordtcnvNEW  33905  ordtrest2NEW  33908  xrge0iifiso  33920  erdszelem9  35181  coepr  35735  dffr5  35736  dfso2  35737  cnvco1  35741  cnvco2  35742  pocnv  35745  txpss3v  35861  brtxp  35863  brpprod3b  35870  idsset  35873  fixcnv  35891  brimage  35909  brcup  35922  brcap  35923  dfrecs2  35933  dfrdg4  35934  dfint3  35935  imagesset  35936  brlb  35938  fvline  36127  ellines  36135  trer  36299  poimirlem31  37640  poimir  37642  frinfm  37724  xrnss3v  38349  rencldnfilem  42803  cnvssco  43590  psshepw  43772  dffrege115  43962  frege131  43978  frege133  43980  brpermmodel  44988  lambert0  46883  lamberte  46884  gte-lteh  49710  gt-lth  49711