Metamath Proof Explorer


Theorem dfsymrel4

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

Ref Expression
Assertion dfsymrel4 ( SymRel 𝑅 ↔ ( 𝑅 = 𝑅 ∧ Rel 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dfsymrel2 ( SymRel 𝑅 ↔ ( 𝑅𝑅 ∧ Rel 𝑅 ) )
2 relcnveq ( Rel 𝑅 → ( 𝑅𝑅 𝑅 = 𝑅 ) )
3 2 pm5.32ri ( ( 𝑅𝑅 ∧ Rel 𝑅 ) ↔ ( 𝑅 = 𝑅 ∧ Rel 𝑅 ) )
4 1 3 bitri ( SymRel 𝑅 ↔ ( 𝑅 = 𝑅 ∧ Rel 𝑅 ) )