Theorem brcnv 5836

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 5833	. 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  5839  dfrn2  5842  dfdm4  5849  cnvsym  6073  cnvsymOLD  6074  cnvsymOLDOLD  6075  intasym  6076  asymref  6077  qfto  6082  dminss  6114  imainss  6115  dminxp  6141  cnvcnv3  6149  cnvpo  6248  cnvso  6249  dffun2  6509  dffun2OLD  6510  funcnvsn  6550  funcnv2  6568  fun2cnv  6571  imadif  6584  f1ompt  7065  foeqcnvco  7257  f1eqcocnv  7258  fliftcnv  7268  isocnv2  7288  fsplit  8073  ercnv  8669  ecid  8730  omxpenlem  9019  sbthcl  9040  fimax2g  9209  dfsup2  9371  eqinf  9412  infval  9414  infcllem  9415  wofib  9474  oemapso  9613  cflim2  10194  fin23lem40  10282  isfin1-3  10317  fin12  10344  negiso  12141  dfinfre  12142  infrenegsup  12144  xrinfmss2  13249  trclublem  14938  imasleval  17481  invsym2  17706  oppcsect2  17722  oduprs  18242  odupos  18268  oduposb  18269  odulub  18347  oduglb  18349  posglbdg  18355  gsumcom3  19893  ordtbas2  23112  ordtcnv  23122  ordtrest2  23125  utop2nei  24172  utop3cls  24173  dvlt0  25944  dvcnvrelem1  25956  nomaxmo  27644  ofpreima  32640  funcnvmpt  32642  odutos  32941  tosglblem  32947  mgccnv  32972  ordtcnvNEW  33904  ordtrest2NEW  33907  xrge0iifiso  33919  erdszelem9  35180  coepr  35734  dffr5  35735  dfso2  35736  cnvco1  35740  cnvco2  35741  pocnv  35744  txpss3v  35860  brtxp  35862  brpprod3b  35869  idsset  35872  fixcnv  35890  brimage  35908  brcup  35921  brcap  35922  dfrecs2  35932  dfrdg4  35933  dfint3  35934  imagesset  35935  brlb  35937  fvline  36126  ellines  36134  trer  36298  poimirlem31  37639  poimir  37641  frinfm  37723  xrnss3v  38348  rencldnfilem  42802  cnvssco  43589  psshepw  43771  dffrege115  43961  frege131  43977  frege133  43979  brpermmodel  44987  lambert0  46882  lamberte  46883  gte-lteh  49709  gt-lth  49710