Theorem brcnv 5832

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3441   class class class wbr 5099  ^◡ccnv 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-cnv 5633

This theorem is referenced by:  cnvco  5835  dfrn2  5838  dfdm4  5845  cnvsym  6072  intasym  6073  asymref  6074  qfto  6079  dminss  6112  imainss  6113  dminxp  6139  cnvcnv3  6147  cnvpo  6246  cnvso  6247  dffun2  6503  funcnvsn  6543  funcnv2  6561  fun2cnv  6564  imadif  6577  funcnvmpt  6944  f1ompt  7058  foeqcnvco  7248  f1eqcocnv  7249  fliftcnv  7259  isocnv2  7279  fsplit  8061  ercnv  8659  ecid  8721  omxpenlem  9010  sbthcl  9031  fimax2g  9190  dfsup2  9351  eqinf  9392  infval  9394  infcllem  9395  wofib  9454  oemapso  9595  cflim2  10177  fin23lem40  10265  isfin1-3  10300  fin12  10327  negiso  12126  dfinfre  12127  infrenegsup  12129  xrinfmss2  13230  trclublem  14922  imasleval  17466  invsym2  17691  oppcsect2  17707  oduprs  18227  odupos  18253  oduposb  18254  odulub  18332  oduglb  18334  posglbdg  18340  chnrev  18554  gsumcom3  19911  ordtbas2  23139  ordtcnv  23149  ordtrest2  23152  utop2nei  24198  utop3cls  24199  dvlt0  25970  dvcnvrelem1  25982  nomaxmo  27670  ofpreima  32746  odutos  33052  tosglblem  33058  mgccnv  33083  ordtcnvNEW  34079  ordtrest2NEW  34082  xrge0iifiso  34094  erdszelem9  35395  coepr  35949  dffr5  35950  dfso2  35951  cnvco1  35955  cnvco2  35956  pocnv  35959  txpss3v  36072  brtxp  36074  brpprod3b  36081  idsset  36084  fixcnv  36102  brimage  36120  brcup  36133  brcap  36134  dfrecs2  36146  dfrdg4  36147  dfint3  36148  imagesset  36149  brlb  36151  fvline  36340  ellines  36348  trer  36512  poimirlem31  37854  poimir  37856  frinfm  37938  xrnss3v  38584  rencldnfilem  43129  cnvssco  43914  psshepw  44096  dffrege115  44286  frege131  44302  frege133  44304  brpermmodel  45311  lambert0  47200  lamberte  47201  gte-lteh  50038  gt-lth  50039