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 ) ) )