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

Metamath Proof Explorer

Theorem dfsymrels3

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

Ref Expression
Assertion dfsymrels3 ⊢ SymRels = r ∈ Rels | ∀ x ∀ y x r y → y r x

Proof

Step Hyp Ref Expression
1 dfsymrels2 ⊢ SymRels = r ∈ Rels | r -1 ⊆ r
2 cnvsym ⊢ r -1 ⊆ r ↔ ∀ x ∀ y x r y → y r x
3 1 2 rabbieq ⊢ SymRels = r ∈ Rels | ∀ x ∀ y x r y → y r x