Theorem brcnv 5868

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

Syntax hints:   ↔ wb 209   ∈ wcel 2141  Vcvv 3453   class class class wbr 5108  ^◡ccnv 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-cnv 5669

This theorem is referenced by:  cnvco  5875  dfrn2  5878  dfdm4  5885  cnvsym  6114  intasym  6115  asymref  6116  qfto  6121  dminss  6150  imainss  6151  xpdifcnvepel  6166  dminxp  6178  cnvcnv3  6186  cnvpo  6288  cnvso  6289  dffun2  6546  funcnvsn  6586  funcnv2  6604  fun2cnv  6607  imadif  6620  funcnvmpt  6991  f1ompt  7106  foeqcnvco  7298  f1eqcocnv  7299  fliftcnv  7309  isocnv2  7329  fsplit  8111  ercnv  8715  ecid  8777  omxpenlem  9065  sbthcl  9086  fimax2g  9245  dfsup2  9403  eqinf  9444  infval  9446  infcllem  9447  wofib  9506  oemapso  9650  cflim2  10246  fin23lem40  10334  isfin1-3  10369  fin12  10396  negiso  12194  dfinfre  12195  infrenegsup  12197  xrinfmss2  13336  trclublem  15031  imasleval  17594  invsym2  17819  oppcsect2  17835  oduprs  18355  odupos  18381  oduposb  18382  odulub  18460  oduglb  18462  posglbdg  18468  chnrev  18682  gsumcom3  20047  ordtbas2  23327  ordtcnv  23337  ordtrest2  23340  utop2nei  24386  utop3cls  24387  dvlt0  26143  dvcnvrelem1  26155  nomaxmo  27838  ofpreima  32976  odutos  33254  tosglblem  33260  mgccnv  33285  ordtcnvNEW  34276  ordtrest2NEW  34279  xrge0iifiso  34291  erdszelem9  35645  coepr  36199  dffr5  36200  dfso2  36201  cnvco1  36205  cnvco2  36206  pocnv  36209  txpss3v  36322  brtxp  36324  brpprod3b  36331  idsset  36334  fixcnv  36352  brimage  36370  brcup  36383  brcap  36384  dfrecs2  36396  dfrdg4  36397  dfint3  36398  imagesset  36399  brlb  36401  fvline  36590  ellines  36598  trer  36771  poimirlem31  38246  poimir  38248  frinfm  38330  xrnss3v  38976  rencldnfilem  43495  cnvssco  44280  psshepw  44462  dffrege115  44652  frege131  44668  frege133  44670  brpermmodel  45660  lambert0  47569  lamberte  47570  gte-lteh  50449  gt-lth  50450