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 <-> A. x A. y ( x R y -> y R x ) ) )

Proof

Step Hyp Ref Expression
1 eqss
 |-  ( R = `' R <-> ( R C_ `' R /\ `' R C_ R ) )
2 cnvsym
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
3 2 biimpi
 |-  ( `' R C_ R -> A. x A. y ( x R y -> y R x ) )
4 3 a1d
 |-  ( `' R C_ R -> ( Rel R -> A. x A. y ( x R y -> y R x ) ) )
5 4 adantl
 |-  ( ( R C_ `' R /\ `' R C_ R ) -> ( Rel R -> A. x A. y ( x R y -> y R x ) ) )
6 5 com12
 |-  ( Rel R -> ( ( R C_ `' R /\ `' R C_ R ) -> A. x A. y ( x R y -> y R x ) ) )
7 dfrel2
 |-  ( Rel R <-> `' `' R = R )
8 cnvss
 |-  ( `' R C_ R -> `' `' R C_ `' R )
9 sseq1
 |-  ( `' `' R = R -> ( `' `' R C_ `' R <-> R C_ `' R ) )
10 8 9 syl5ibcom
 |-  ( `' R C_ R -> ( `' `' R = R -> R C_ `' R ) )
11 2 10 sylbir
 |-  ( A. x A. y ( x R y -> y R x ) -> ( `' `' R = R -> R C_ `' R ) )
12 11 com12
 |-  ( `' `' R = R -> ( A. x A. y ( x R y -> y R x ) -> R C_ `' R ) )
13 7 12 sylbi
 |-  ( Rel R -> ( A. x A. y ( x R y -> y R x ) -> R C_ `' R ) )
14 2 biimpri
 |-  ( A. x A. y ( x R y -> y R x ) -> `' R C_ R )
15 13 14 jca2
 |-  ( Rel R -> ( A. x A. y ( x R y -> y R x ) -> ( R C_ `' R /\ `' R C_ R ) ) )
16 6 15 impbid
 |-  ( Rel R -> ( ( R C_ `' R /\ `' R C_ R ) <-> A. x A. y ( x R y -> y R x ) ) )
17 1 16 syl5bb
 |-  ( Rel R -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) )