This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfsymrels5

Description: Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021)

Ref Expression
Assertion dfsymrels5 ⊢ SymRels = r ∈ Rels | ∀ x ∀ y x r y ↔ y r x

Proof

Step Hyp Ref Expression
1 dfsymrels4 ⊢ SymRels = r ∈ Rels | r -1 = r
2 elrelscnveq2 ⊢ r ∈ Rels → r -1 = r ↔ ∀ x ∀ y x r y ↔ y r x
3 1 2 rabimbieq ⊢ SymRels = r ∈ Rels | ∀ x ∀ y x r y ↔ y r x