Theorem dfsymrels5

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

	Ref	Expression
Assertion	dfsymrels5	⊢ SymRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }

Proof

Step	Hyp	Ref	Expression
1		dfsymrels4	⊢ SymRels = { 𝑟 ∈ Rels ∣ ◡ 𝑟 = 𝑟 }
2		elrelscnveq2	⊢ ( 𝑟 ∈ Rels → ( ◡ 𝑟 = 𝑟 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ) )
3	1 2	rabimbieq	⊢ SymRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }