Theorem elsymrels3

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

	Ref	Expression
Assertion	elsymrels3	⊢ ( 𝑅 ∈ SymRels ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dfsymrels3	⊢ SymRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) }
2		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
3		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑦 𝑟 𝑥 ↔ 𝑦 𝑅 𝑥 ) )
4	2 3	imbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
5	4	2albidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
6	1 5	rabeqel	⊢ ( 𝑅 ∈ SymRels ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ 𝑅 ∈ Rels ) )