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 -> ( R e. Rels -> A. x A. y ( x R y -> y R x ) ) ) |
5 |
4
|
adantl |
|- ( ( R C_ `' R /\ `' R C_ R ) -> ( R e. Rels -> A. x A. y ( x R y -> y R x ) ) ) |
6 |
5
|
com12 |
|- ( R e. Rels -> ( ( R C_ `' R /\ `' R C_ R ) -> A. x A. y ( x R y -> y R x ) ) ) |
7 |
|
elrelsrelim |
|- ( R e. Rels -> Rel R ) |
8 |
|
dfrel2 |
|- ( Rel R <-> `' `' R = R ) |
9 |
7 8
|
sylib |
|- ( R e. Rels -> `' `' R = R ) |
10 |
|
cnvss |
|- ( `' R C_ R -> `' `' R C_ `' R ) |
11 |
|
sseq1 |
|- ( `' `' R = R -> ( `' `' R C_ `' R <-> R C_ `' R ) ) |
12 |
10 11
|
syl5ibcom |
|- ( `' R C_ R -> ( `' `' R = R -> R C_ `' R ) ) |
13 |
2 12
|
sylbir |
|- ( A. x A. y ( x R y -> y R x ) -> ( `' `' R = R -> R C_ `' R ) ) |
14 |
9 13
|
syl5com |
|- ( R e. Rels -> ( A. x A. y ( x R y -> y R x ) -> R C_ `' R ) ) |
15 |
2
|
biimpri |
|- ( A. x A. y ( x R y -> y R x ) -> `' R C_ R ) |
16 |
14 15
|
jca2 |
|- ( R e. Rels -> ( A. x A. y ( x R y -> y R x ) -> ( R C_ `' R /\ `' R C_ R ) ) ) |
17 |
6 16
|
impbid |
|- ( R e. Rels -> ( ( R C_ `' R /\ `' R C_ R ) <-> A. x A. y ( x R y -> y R x ) ) ) |
18 |
1 17
|
syl5bb |
|- ( R e. Rels -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) ) |