This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) (Proof shortened by SN, 23-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

Ref Expression
Assertion cnvsym ⊢ R -1 ⊆ R ↔ ∀ x ∀ y x R y → y R x

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ R -1
2 ssrel3 ⊢ Rel ⁡ R -1 → R -1 ⊆ R ↔ ∀ y ∀ x y R -1 x → y R x
3 1 2 ax-mp ⊢ R -1 ⊆ R ↔ ∀ y ∀ x y R -1 x → y R x
4 breq1 ⊢ y = z → y R -1 x ↔ z R -1 x
5 breq1 ⊢ y = z → y R x ↔ z R x
6 4 5 imbi12d ⊢ y = z → y R -1 x → y R x ↔ z R -1 x → z R x
7 breq2 ⊢ x = z → y R -1 x ↔ y R -1 z
8 breq2 ⊢ x = z → y R x ↔ y R z
9 7 8 imbi12d ⊢ x = z → y R -1 x → y R x ↔ y R -1 z → y R z
10 6 9 alcomw ⊢ ∀ y ∀ x y R -1 x → y R x ↔ ∀ x ∀ y y R -1 x → y R x
11 vex ⊢ y ∈ V
12 vex ⊢ x ∈ V
13 11 12 brcnv ⊢ y R -1 x ↔ x R y
14 13 imbi1i ⊢ y R -1 x → y R x ↔ x R y → y R x
15 14 2albii ⊢ ∀ x ∀ y y R -1 x → y R x ↔ ∀ x ∀ y x R y → y R x
16 3 10 15 3bitri ⊢ R -1 ⊆ R ↔ ∀ x ∀ y x R y → y R x