Metamath Proof Explorer

Theorem elrelscnveq2

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion elrelscnveq2 
|- ( R e. Rels -> ( `' R = R <-> A. x A. y ( x R y <-> y R x ) ) )

Proof

Step Hyp Ref Expression
1 cnvsym 
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
2 1 a1i 
 |-  ( R e. Rels -> ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) )
3 elrelsrelim 
 |-  ( R e. Rels -> Rel R )
4 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
5 3 4 sylib 
 |-  ( R e. Rels -> `' `' R = R )
6 5 sseq1d 
 |-  ( R e. Rels -> ( `' `' R C_ `' R <-> R C_ `' R ) )
7 cnvsym 
 |-  ( `' `' R C_ `' R <-> A. x A. y ( x `' R y -> y `' R x ) )
8 6 7 bitr3di 
 |-  ( R e. Rels -> ( R C_ `' R <-> A. x A. y ( x `' R y -> y `' R x ) ) )
9 relbrcnvg 
 |-  ( Rel R -> ( x `' R y <-> y R x ) )
10 3 9 syl 
 |-  ( R e. Rels -> ( x `' R y <-> y R x ) )
11 relbrcnvg 
 |-  ( Rel R -> ( y `' R x <-> x R y ) )
12 3 11 syl 
 |-  ( R e. Rels -> ( y `' R x <-> x R y ) )
13 10 12 imbi12d 
 |-  ( R e. Rels -> ( ( x `' R y -> y `' R x ) <-> ( y R x -> x R y ) ) )
14 13 2albidv 
 |-  ( R e. Rels -> ( A. x A. y ( x `' R y -> y `' R x ) <-> A. x A. y ( y R x -> x R y ) ) )
15 8 14 bitrd 
 |-  ( R e. Rels -> ( R C_ `' R <-> A. x A. y ( y R x -> x R y ) ) )
16 2 15 anbi12d 
 |-  ( R e. Rels -> ( ( `' R C_ R /\ R C_ `' R ) <-> ( A. x A. y ( x R y -> y R x ) /\ A. x A. y ( y R x -> x R y ) ) ) )
17 eqss 
 |-  ( `' R = R <-> ( `' R C_ R /\ R C_ `' R ) )
18 2albiim 
 |-  ( A. x A. y ( x R y <-> y R x ) <-> ( A. x A. y ( x R y -> y R x ) /\ A. x A. y ( y R x -> x R y ) ) )
19 16 17 18 3bitr4g 
 |-  ( R e. Rels -> ( `' R = R <-> A. x A. y ( x R y <-> y R x ) ) )