Theorem dfsymrel5

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

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

Proof

Step	Hyp	Ref	Expression
1		dfsymrel2	⊢ ( SymRel 𝑅 ↔ ( ◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) )
2		relcnveq4	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )
3	2	pm5.32ri	⊢ ( ( ◡ 𝑅 ⊆ 𝑅 ∧ Rel 𝑅 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) )
4	1 3	bitri	⊢ ( SymRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ∧ Rel 𝑅 ) )