Metamath Proof Explorer

Theorem elrelscnveq

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

Ref Expression
Assertion elrelscnveq 
|- ( R e. Rels -> ( `' R C_ R <-> `' R = R ) )

Proof

Step Hyp Ref Expression
1 elrelscnveq3 
 |-  ( R e. Rels -> ( 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 
 |-  ( R e. Rels -> ( R = `' R <-> `' R C_ R ) )
4 eqcom 
 |-  ( R = `' R <-> `' R = R )
5 3 4 bitr3di 
 |-  ( R e. Rels -> ( `' R C_ R <-> `' R = R ) )