Theorem elrelscnveq4

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

	Ref	Expression
Assertion	elrelscnveq4	⊢ ( 𝑅 ∈ Rels → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elrelscnveq	⊢ ( 𝑅 ∈ Rels → ( ◡ 𝑅 ⊆ 𝑅 ↔ ◡ 𝑅 = 𝑅 ) )
2		elrelscnveq2	⊢ ( 𝑅 ∈ Rels → ( ◡ 𝑅 = 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )
3	1 2	bitrd	⊢ ( 𝑅 ∈ Rels → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )