Theorem brcnv 5864

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3450   class class class wbr 5103  ^◡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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663

This theorem is used by:  cnvco  5871  dfrn2  5874  dfdm4  5881  cnvsym  6110  intasym  6111  asymref  6112  qfto  6117  dminss  6146  imainss  6147  cnvxp  6150  xpdifcnvepel  6163  dminxp  6175  cnvcnv3  6183  cnvpo  6287  cnvso  6288  dffun2  6545  funcnvsn  6586  funcnv2  6604  fun2cnv  6607  imadif  6620  funcnvmpt  6991  f1ompt  7107  foeqcnvco  7304  f1eqcocnv  7305  fliftcnv  7315  isocnv2  7335  fsplit  8119  ercnv  8725  ecid  8787  omxpenlem  9083  sbthcl  9104  fimax2g  9263  dfsup2  9421  eqinf  9462  infval  9464  infcllem  9465  wofib  9524  oemapso  9668  cflim2  10290  fin23lem40  10378  isfin1-3  10413  fin12  10440  negiso  12244  dfinfre  12245  infrenegsup  12247  xrinfmss2  13388  trclublem  15093  imasleval  17652  invsym2  17877  oppcsect2  17893  oduprs  18413  odupos  18439  oduposb  18440  odulub  18518  oduglb  18520  posglbdg  18526  chnrev  18740  gsumcom3  20131  ordtbas2  23448  ordtcnv  23458  ordtrest2  23461  utop2nei  24508  utop3cls  24509  dvlt0  26264  dvcnvrelem1  26276  nomaxmo  27966  ofpreima  33170  odutos  33440  tosglblem  33446  mgccnv  33471  ordtcnvNEW  34463  ordtrest2NEW  34466  xrge0iifiso  34478  erdszelem9  35861  coepr  36415  dffr5  36416  dfso2  36417  cnvco1  36421  cnvco2  36422  pocnv  36425  txpss3v  36538  brtxp  36540  brpprod3b  36547  idsset  36550  fixcnv  36568  brimage  36586  brcup  36599  brcap  36600  dfrecs2  36612  dfrdg4  36613  dfint3  36614  imagesset  36615  brlb  36617  fvline  36807  ellines  36815  trer  37002  poimirlem31  38465  poimir  38467  frinfm  38550  xrnss3v  39194  rencldnfilem  43726  cnvssco  44511  psshepw  44693  dffrege115  44883  frege131  44899  frege133  44901  brpermmodel  45891  lambert0  47820  lamberte  47821  gte-lteh  50717  gt-lth  50718