Metamath Proof Explorer


Theorem relcnveq3

Description: Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009)

Ref Expression
Assertion relcnveq3 Rel R R = R -1 x y x R y y R x

Proof

Step Hyp Ref Expression
1 eqss R = R -1 R R -1 R -1 R
2 cnvsym R -1 R x y x R y y R x
3 2 biimpi R -1 R x y x R y y R x
4 3 a1d R -1 R Rel R x y x R y y R x
5 4 adantl R R -1 R -1 R Rel R x y x R y y R x
6 5 com12 Rel R R R -1 R -1 R x y x R y y R x
7 dfrel2 Rel R R -1 -1 = R
8 cnvss R -1 R R -1 -1 R -1
9 sseq1 R -1 -1 = R R -1 -1 R -1 R R -1
10 8 9 syl5ibcom R -1 R R -1 -1 = R R R -1
11 2 10 sylbir x y x R y y R x R -1 -1 = R R R -1
12 11 com12 R -1 -1 = R x y x R y y R x R R -1
13 7 12 sylbi Rel R x y x R y y R x R R -1
14 2 biimpri x y x R y y R x R -1 R
15 13 14 jca2 Rel R x y x R y y R x R R -1 R -1 R
16 6 15 impbid Rel R R R -1 R -1 R x y x R y y R x
17 1 16 syl5bb Rel R R = R -1 x y x R y y R x