Theorem cnvsym

Description: Two ways of saying a relation is symmetric. Similar to definition of symmetry in Schechter p. 51. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by SN, 23-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ 𝑅
2		ssrel3	⊢ ( Rel ◡ 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ) )
3	1 2	ax-mp	⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) )
4		breq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑧 ◡ 𝑅 𝑥 ) )
5		breq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑧 𝑅 𝑥 ) )
6	4 5	imbi12d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ( 𝑧 ◡ 𝑅 𝑥 → 𝑧 𝑅 𝑥 ) ) )
7		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑦 ◡ 𝑅 𝑧 ) )
8		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑧 ) )
9	7 8	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ( 𝑦 ◡ 𝑅 𝑧 → 𝑦 𝑅 𝑧 ) ) )
10	6 9	alcomw	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) )
11		vex	⊢ 𝑦 ∈ V
12		vex	⊢ 𝑥 ∈ V
13	11 12	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
14	13	imbi1i	⊢ ( ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
15	14	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
16	3 10 15	3bitri	⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )