Metamath Proof Explorer

Theorem elrelscnveq4

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

Ref Expression
Assertion elrelscnveq4 
|- ( R e. Rels -> ( `' R C_ R <-> A. x A. y ( x R y <-> y R x ) ) )

Proof

Step Hyp Ref Expression
1 elrelscnveq 
 |-  ( R e. Rels -> ( `' R C_ R <-> `' R = R ) )
2 elrelscnveq2 
 |-  ( R e. Rels -> ( `' R = R <-> A. x A. y ( x R y <-> y R x ) ) )
3 1 2 bitrd 
 |-  ( R e. Rels -> ( `' R C_ R <-> A. x A. y ( x R y <-> y R x ) ) )