Metamath Proof Explorer


Theorem dfsymrels4

Description: Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019)

Ref Expression
Assertion dfsymrels4 SymRels = { 𝑟 ∈ Rels ∣ 𝑟 = 𝑟 }

Proof

Step Hyp Ref Expression
1 dfsymrels2 SymRels = { 𝑟 ∈ Rels ∣ 𝑟𝑟 }
2 elrelscnveq ( 𝑟 ∈ Rels → ( 𝑟𝑟 𝑟 = 𝑟 ) )
3 1 2 rabimbieq SymRels = { 𝑟 ∈ Rels ∣ 𝑟 = 𝑟 }