Theorem brcnv 5866

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3453   class class class wbr 5107  ^◡ccnv 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-cnv 5667

This theorem is used by:  cnvco  5873  dfrn2  5876  dfdm4  5883  cnvsym  6112  intasym  6113  asymref  6114  qfto  6119  dminss  6148  imainss  6149  cnvxp  6152  xpdifcnvepel  6165  dminxp  6177  cnvcnv3  6185  cnvpo  6289  cnvso  6290  dffun2  6547  funcnvsn  6587  funcnv2  6605  fun2cnv  6608  imadif  6621  funcnvmpt  6992  f1ompt  7107  foeqcnvco  7304  f1eqcocnv  7305  fliftcnv  7315  isocnv2  7335  fsplit  8117  ercnv  8721  ecid  8783  omxpenlem  9079  sbthcl  9100  fimax2g  9259  dfsup2  9417  eqinf  9458  infval  9460  infcllem  9461  wofib  9520  oemapso  9664  cflim2  10268  fin23lem40  10356  isfin1-3  10391  fin12  10418  negiso  12220  dfinfre  12221  infrenegsup  12223  xrinfmss2  13363  trclublem  15068  imasleval  17629  invsym2  17854  oppcsect2  17870  oduprs  18390  odupos  18416  oduposb  18417  odulub  18495  oduglb  18497  posglbdg  18503  chnrev  18717  gsumcom3  20104  ordtbas2  23415  ordtcnv  23425  ordtrest2  23428  utop2nei  24475  utop3cls  24476  dvlt0  26232  dvcnvrelem1  26244  nomaxmo  27930  ofpreima  33123  odutos  33393  tosglblem  33399  mgccnv  33424  ordtcnvNEW  34415  ordtrest2NEW  34418  xrge0iifiso  34430  erdszelem9  35763  coepr  36317  dffr5  36318  dfso2  36319  cnvco1  36323  cnvco2  36324  pocnv  36327  txpss3v  36440  brtxp  36442  brpprod3b  36449  idsset  36452  fixcnv  36470  brimage  36488  brcup  36501  brcap  36502  dfrecs2  36514  dfrdg4  36515  dfint3  36516  imagesset  36517  brlb  36519  fvline  36709  ellines  36717  trer  36920  poimirlem31  38385  poimir  38387  frinfm  38470  xrnss3v  39114  rencldnfilem  43646  cnvssco  44431  psshepw  44613  dffrege115  44803  frege131  44819  frege133  44821  brpermmodel  45811  lambert0  47740  lamberte  47741  gte-lteh  50637  gt-lth  50638