Theorem dfsymrels3

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

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

Proof

Step	Hyp	Ref	Expression
1		dfsymrels2	⊢ SymRels = { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 }
2		cnvsym	⊢ ( ◡ 𝑟 ⊆ 𝑟 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) )
3	1 2	rabbieq	⊢ SymRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) }