Metamath Proof Explorer


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 ) )