Theorem relcnveq4

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019)

	Ref	Expression
Assertion	relcnveq4	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		relcnveq	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ◡ 𝑅 = 𝑅 ) )
2		relcnveq2	⊢ ( Rel 𝑅 → ( ◡ 𝑅 = 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )
3	1 2	bitrd	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )