Metamath Proof Explorer

Theorem elsymrels2

Description: Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021)

Ref Expression
Assertion elsymrels2 
|- ( R e. SymRels <-> ( `' R C_ R /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 dfsymrels2 
 |-  SymRels = { r e. Rels | `' r C_ r }
2 cnveq 
 |-  ( r = R -> `' r = `' R )
3 id 
 |-  ( r = R -> r = R )
4 2 3 sseq12d 
 |-  ( r = R -> ( `' r C_ r <-> `' R C_ R ) )
5 1 4 rabeqel 
 |-  ( R e. SymRels <-> ( `' R C_ R /\ R e. Rels ) )