Metamath Proof Explorer


Theorem dfsymrel3

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

Ref Expression
Assertion dfsymrel3 ( SymRel 𝑅 ↔ ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dfsymrel2 ( SymRel 𝑅 ↔ ( 𝑅𝑅 ∧ Rel 𝑅 ) )
2 cnvsym ( 𝑅𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
3 2 anbi1i ( ( 𝑅𝑅 ∧ Rel 𝑅 ) ↔ ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) )
4 1 3 bitri ( SymRel 𝑅 ↔ ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) )