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