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