Theorem brcnv 5866

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  Vcvv 3454   class class class wbr 5106  ^◡ccnv 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-cnv 5663

This theorem is used by:  cnvco  5873  dfrn2  5876  dfdm4  5883  cnvsym  6119  intasym  6120  asymref  6121  qfto  6126  dminss  6154  imainss  6155  cnvxp  6158  xpdifcnvepel  6171  dminxp  6183  cnvcnv3  6191  idresdmsscocnv1  6274  cnvpo  6305  cnvso  6306  dffun2  6565  funcnvsn  6609  funcnv2  6627  fun2cnv  6630  imadif  6643  funcnvmpt  7015  f1ompt  7132  foeqcnvco  7328  f1eqcocnv  7329  fliftcnv  7339  isocnv2  7359  fsplit  8152  ercnv  8764  ecid  8826  omxpenlem  9122  sbthcl  9143  fimax2g  9302  dfsup2  9460  eqinf  9501  infval  9503  infcllem  9504  wofib  9563  oemapso  9707  cflim2  10365  fin23lem40  10453  isfin1-3  10488  fin12  10515  negiso  12321  dfinfre  12322  infrenegsup  12324  xrinfmss2  13465  trclublem  15174  imasleval  17739  invsym2  17964  oppcsect2  17980  oduprs  18500  odupos  18526  oduposb  18527  odulub  18605  oduglb  18607  posglbdg  18613  chnrev  18827  gsumcom3  20219  ordtbas2  23536  ordtcnv  23546  ordtrest2  23549  utop2nei  24596  utop3cls  24597  dvlt0  26352  dvcnvrelem1  26364  nomaxmo  28082  ofpreima  33328  odutos  33596  tosglblem  33602  mgccnv  33627  ordtcnvNEW  34619  ordtrest2NEW  34622  xrge0iifiso  34634  erdszelem9  36130  coepr  36695  dffr5  36696  dfso2  36697  cnvco1  36701  cnvco2  36702  pocnv  36705  txpss3v  36817  brtxp  36819  brpprod3b  36826  idsset  36829  fixcnv  36847  brimage  36865  brcup  36878  brcap  36879  dfrecs2  36891  dfrdg4  36892  dfint3  36893  imagesset  36894  brlb  36896  fvline  37086  ellines  37094  trer  37281  poimirlem31  38760  poimir  38762  frinfm  38860  xrnss3v  39504  rencldnfilem  44018  cnvssco  44796  psshepw  44978  dffrege115  45168  frege131  45184  frege133  45186  brpermmodel  46186  lambert0  48140  lamberte  48141  gte-lteh  51097  gt-lth  51098