Metamath Proof Explorer


Theorem elsymrels2

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

Ref Expression
Assertion elsymrels2 ( 𝑅 ∈ SymRels ↔ ( 𝑅𝑅𝑅 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 dfsymrels2 SymRels = { 𝑟 ∈ Rels ∣ 𝑟𝑟 }
2 cnveq ( 𝑟 = 𝑅 𝑟 = 𝑅 )
3 id ( 𝑟 = 𝑅𝑟 = 𝑅 )
4 2 3 sseq12d ( 𝑟 = 𝑅 → ( 𝑟𝑟 𝑅𝑅 ) )
5 1 4 rabeqel ( 𝑅 ∈ SymRels ↔ ( 𝑅𝑅𝑅 ∈ Rels ) )