Theorem brcnv 5883

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   class class class wbr 5149  ^◡ccnv 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685

This theorem is referenced by:  cnvco  5886  dfrn2  5889  dfdm4  5896  cnvsym  6114  cnvsymOLD  6115  cnvsymOLDOLD  6116  intasym  6117  asymref  6118  qfto  6123  dminss  6153  imainss  6154  dminxp  6180  cnvcnv3  6188  cnvpo  6287  cnvso  6288  dffun2  6554  dffun2OLD  6555  dffun2OLDOLD  6556  funcnvsn  6599  funcnv2  6617  fun2cnv  6620  imadif  6633  f1ompt  7111  foeqcnvco  7298  f1eqcocnv  7299  f1eqcocnvOLD  7300  fliftcnv  7308  isocnv2  7328  fsplit  8103  ercnv  8724  ecid  8776  omxpenlem  9073  sbthcl  9095  fimax2g  9289  dfsup2  9439  eqinf  9479  infval  9481  infcllem  9482  wofib  9540  oemapso  9677  cflim2  10258  fin23lem40  10346  isfin1-3  10381  fin12  10408  negiso  12194  dfinfre  12195  infrenegsup  12197  xrinfmss2  13290  trclublem  14942  imasleval  17487  invsym2  17710  oppcsect2  17726  odupos  18281  oduposb  18282  odulub  18360  oduglb  18362  posglbdg  18368  gsumcom3  19846  ordtbas2  22695  ordtcnv  22705  ordtrest2  22708  utop2nei  23755  utop3cls  23756  dvlt0  25522  dvcnvrelem1  25534  nomaxmo  27201  ofpreima  31890  funcnvmpt  31892  oduprs  32134  odutos  32138  tosglblem  32144  mgccnv  32169  ordtcnvNEW  32900  ordtrest2NEW  32903  xrge0iifiso  32915  erdszelem9  34190  coepr  34723  dffr5  34724  dfso2  34725  cnvco1  34729  cnvco2  34730  pocnv  34733  txpss3v  34850  brtxp  34852  brpprod3b  34859  idsset  34862  fixcnv  34880  brimage  34898  brcup  34911  brcap  34912  dfrecs2  34922  dfrdg4  34923  dfint3  34924  imagesset  34925  brlb  34927  fvline  35116  ellines  35124  trer  35201  poimirlem31  36519  poimir  36521  frinfm  36603  xrnss3v  37242  rencldnfilem  41558  cnvssco  42357  psshepw  42539  dffrege115  42729  frege131  42745  frege133  42747  gte-lteh  47771  gt-lth  47772