Metamath Proof Explorer

Theorem elsymrels5

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

Ref Expression
Assertion elsymrels5 ⊢ R ∈ SymRels ↔ ∀ x ∀ y x R y ↔ y R x ∧ R ∈ Rels

Proof

Step Hyp Ref Expression
1 dfsymrels5 ⊢ SymRels = r ∈ Rels | ∀ x ∀ y x r y ↔ y r x
2 breq ⊢ r = R → x r y ↔ x R y
3 breq ⊢ r = R → y r x ↔ y R x
4 2 3 bibi12d ⊢ r = R → x r y ↔ y r x ↔ x R y ↔ y R x
5 4 2albidv ⊢ r = R → ∀ x ∀ y x r y ↔ y r x ↔ ∀ x ∀ y x R y ↔ y R x
6 1 5 rabeqel ⊢ R ∈ SymRels ↔ ∀ x ∀ y x R y ↔ y R x ∧ R ∈ Rels