Metamath Proof Explorer

Theorem brcnvg

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

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

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = A -> ( y R x <-> y R A ) )
2 breq1 
 |-  ( y = B -> ( y R A <-> B R A ) )
3 df-cnv 
 |-  `' R = { <. x , y >. | y R x }
4 1 2 3 brabg 
 |-  ( ( A e. C /\ B e. D ) -> ( A `' R B <-> B R A ) )