Theorem relcnveq

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018)

	Ref	Expression
Assertion	relcnveq	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ◡ 𝑅 = 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relcnveq3	⊢ ( Rel 𝑅 → ( 𝑅 = ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
2		cnvsym	⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
3	1 2	bitr4di	⊢ ( Rel 𝑅 → ( 𝑅 = ◡ 𝑅 ↔ ◡ 𝑅 ⊆ 𝑅 ) )
4		eqcom	⊢ ( 𝑅 = ◡ 𝑅 ↔ ◡ 𝑅 = 𝑅 )
5	3 4	bitr3di	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ◡ 𝑅 = 𝑅 ) )