Description: Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | elsymrels5 | ⊢ ( 𝑅 ∈ SymRels ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ∧ 𝑅 ∈ Rels ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsymrels5 | ⊢ SymRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) } | |
2 | breq | ⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) ) | |
3 | breq | ⊢ ( 𝑟 = 𝑅 → ( 𝑦 𝑟 𝑥 ↔ 𝑦 𝑅 𝑥 ) ) | |
4 | 2 3 | bibi12d | ⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ) |
5 | 4 | 2albidv | ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ) |
6 | 1 5 | rabeqel | ⊢ ( 𝑅 ∈ SymRels ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ∧ 𝑅 ∈ Rels ) ) |