Metamath Proof Explorer

Theorem relcnveq

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018)

Ref Expression
Assertion relcnveq 
|- ( Rel R -> ( `' R C_ R <-> `' R = R ) )

Proof

Step Hyp Ref Expression
1 relcnveq3 
 |-  ( Rel R -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) )
2 cnvsym 
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
3 1 2 bitr4di 
 |-  ( Rel R -> ( R = `' R <-> `' R C_ R ) )
4 eqcom 
 |-  ( R = `' R <-> `' R = R )
5 3 4 bitr3di 
 |-  ( Rel R -> ( `' R C_ R <-> `' R = R ) )