Theorem brcnv 5444

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

Syntax hints:   ↔ wb 196   ∈ wcel 2145  Vcvv 3351   class class class wbr 4787  ^◡ccnv 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4788  df-opab 4848  df-cnv 5258

This theorem is referenced by:  cnvco  5447  dfrn2  5450  dfdm4  5455  cnvsym  5652  intasym  5653  asymref  5654  qfto  5659  dminss  5689  imainss  5690  dminxp  5716  cnvcnv3  5724  cnvpo  5818  cnvso  5819  dffun2  6042  funcnvsn  6080  funcnv2  6098  fun2cnv  6101  imadif  6114  f1ompt  6525  foeqcnvco  6699  f1eqcocnv  6700  fliftcnv  6705  isocnv2  6725  fsplit  7434  ercnv  7918  ecid  7965  omxpenlem  8218  sbthcl  8239  fimax2g  8363  dfsup2  8507  eqinf  8547  infval  8549  infcllem  8550  wofib  8607  oemapso  8744  cflim2  9288  fin23lem40  9376  isfin1-3  9411  fin12  9438  negiso  11206  dfinfre  11207  infrenegsup  11209  xrinfmss2  12347  trclublem  13945  imasleval  16410  invsym2  16631  oppcsect2  16647  odupos  17344  oduposb  17345  oduglb  17348  odulub  17350  posglbd  17359  gsumcom3  20423  ordtbas2  21217  ordtcnv  21227  ordtrest2  21230  utop2nei  22275  utop3cls  22276  dvlt0  23989  dvcnvrelem1  24001  ofpreima  29806  funcnvmptOLD  29808  funcnvmpt  29809  oduprs  29997  odutos  30004  tosglblem  30010  ordtcnvNEW  30307  ordtrest2NEW  30310  xrge0iifiso  30322  erdszelem9  31520  coepr  31981  dffr5  31982  dfso2  31983  cnvco1  31988  cnvco2  31989  pocnv  31992  nomaxmo  32185  txpss3v  32323  brtxp  32325  brpprod3b  32332  idsset  32335  fixcnv  32353  brimage  32371  brcup  32384  brcap  32385  dfrecs2  32395  dfrdg4  32396  dfint3  32397  imagesset  32398  brlb  32400  fvline  32589  ellines  32597  trer  32648  gtinfOLD  32652  poimirlem31  33774  poimir  33776  frinfm  33863  xrnss3v  34477  rencldnfilem  37911  cnvssco  38439  psshepw  38609  dffrege115  38799  frege131  38815  frege133  38817  gte-lteh  42999  gt-lth  43000