Theorem brcnvg 5303

Description: The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)

Assertion

Ref	Expression
brcnvg	|- ( ( A e. C /\ B e. D ) -> ( A `' R B <-> B R A ) )

Proof of Theorem brcnvg

Step	Hyp	Ref	Expression
1		opelcnvg 5302	. 2 |- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. `' R <-> <. B , A >. e. R ) )
2		df-br 4654	. 2 |- ( A `' R B <-> <. A , B >. e. `' R )
3		df-br 4654	. 2 |- ( B R A <-> <. B , A >. e. R )
4	1, 2, 3	3bitr4g 303	1 |- ( ( A e. C /\ B e. D ) -> ( A `' R B <-> B R A ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   <.cop 4183   class class class wbr 4653   `'ccnv 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-cnv 5122

This theorem is referenced by:  brcnv  5305  brelrng  5355  eliniseg  5494  relbrcnvg  5504  brcodir  5515  elpredg  5694  predep  5706  dffv2  6271  ersym  7754  brdifun  7771  eqinf  8390  inflb  8395  infglb  8396  infglbb  8397  infltoreq  8408  infempty  8412  brcnvtrclfv  13744  oduleg  17132  posglbd  17150  znleval  19903  brbtwn  25779  fcoinvbr  29419  cnvordtrestixx  29959  xrge0iifiso  29981  orvcgteel  30529  inffzOLD  31615  fv1stcnv  31680  fv2ndcnv  31681  wsuclem  31773  wsuclemOLD  31774  wsuclb  31777  slenlt  31877  colineardim1  32168  gtinfOLD  32314  eldmcnv  34113  ineccnvmo  34122  alrmomo  34123  brnonrel  37895  ntrneifv2  38378  gte-lte  42465  gt-lt  42466