Metamath Proof Explorer


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)

Ref Expression
Assertion cnvsym ( 𝑅𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )

Proof

Step Hyp Ref Expression
1 alcom ( ∀ 𝑦𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) ↔ ∀ 𝑥𝑦 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
2 relcnv Rel 𝑅
3 ssrel ( Rel 𝑅 → ( 𝑅𝑅 ↔ ∀ 𝑦𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) ) )
4 2 3 ax-mp ( 𝑅𝑅 ↔ ∀ 𝑦𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
5 vex 𝑦 ∈ V
6 vex 𝑥 ∈ V
7 5 6 brcnv ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 )
8 df-br ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 )
9 7 8 bitr3i ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 )
10 df-br ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 )
11 9 10 imbi12i ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
12 11 2albii ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥𝑦 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
13 1 4 12 3bitr4i ( 𝑅𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )