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 bitrid 
 |-  ( Rel R -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) )