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 ∣ ◡ 𝑟 = 𝑟 }