Metamath Proof Explorer

Theorem dfsymrel5

Description: Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021)

Ref Expression
Assertion dfsymrel5 ⊢ SymRel R ↔ ∀ x ∀ y x R y ↔ y R x ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 dfsymrel2 ⊢ SymRel R ↔ R -1 ⊆ R ∧ Rel ⁡ R
2 relcnveq4 ⊢ Rel ⁡ R → R -1 ⊆ R ↔ ∀ x ∀ y x R y ↔ y R x
3 2 pm5.32ri ⊢ R -1 ⊆ R ∧ Rel ⁡ R ↔ ∀ x ∀ y x R y ↔ y R x ∧ Rel ⁡ R
4 1 3 bitri ⊢ SymRel R ↔ ∀ x ∀ y x R y ↔ y R x ∧ Rel ⁡ R