Metamath Proof Explorer

Theorem elsymrels3

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

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

Proof

Step Hyp Ref Expression
1 dfsymrels3 ⊢ 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 imbi12d ⊢ 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