Step |
Hyp |
Ref |
Expression |
1 |
|
dfss2 |
|- ( ( _I |` A ) C_ R <-> A. y ( y e. ( _I |` A ) -> y e. R ) ) |
2 |
|
elrid |
|- ( y e. ( _I |` A ) <-> E. x e. A y = <. x , x >. ) |
3 |
2
|
imbi1i |
|- ( ( y e. ( _I |` A ) -> y e. R ) <-> ( E. x e. A y = <. x , x >. -> y e. R ) ) |
4 |
|
r19.23v |
|- ( A. x e. A ( y = <. x , x >. -> y e. R ) <-> ( E. x e. A y = <. x , x >. -> y e. R ) ) |
5 |
|
eleq1 |
|- ( y = <. x , x >. -> ( y e. R <-> <. x , x >. e. R ) ) |
6 |
|
df-br |
|- ( x R x <-> <. x , x >. e. R ) |
7 |
5 6
|
bitr4di |
|- ( y = <. x , x >. -> ( y e. R <-> x R x ) ) |
8 |
7
|
pm5.74i |
|- ( ( y = <. x , x >. -> y e. R ) <-> ( y = <. x , x >. -> x R x ) ) |
9 |
8
|
ralbii |
|- ( A. x e. A ( y = <. x , x >. -> y e. R ) <-> A. x e. A ( y = <. x , x >. -> x R x ) ) |
10 |
3 4 9
|
3bitr2i |
|- ( ( y e. ( _I |` A ) -> y e. R ) <-> A. x e. A ( y = <. x , x >. -> x R x ) ) |
11 |
10
|
albii |
|- ( A. y ( y e. ( _I |` A ) -> y e. R ) <-> A. y A. x e. A ( y = <. x , x >. -> x R x ) ) |
12 |
|
ralcom4 |
|- ( A. x e. A A. y ( y = <. x , x >. -> x R x ) <-> A. y A. x e. A ( y = <. x , x >. -> x R x ) ) |
13 |
|
opex |
|- <. x , x >. e. _V |
14 |
|
biidd |
|- ( y = <. x , x >. -> ( x R x <-> x R x ) ) |
15 |
13 14
|
ceqsalv |
|- ( A. y ( y = <. x , x >. -> x R x ) <-> x R x ) |
16 |
15
|
ralbii |
|- ( A. x e. A A. y ( y = <. x , x >. -> x R x ) <-> A. x e. A x R x ) |
17 |
11 12 16
|
3bitr2i |
|- ( A. y ( y e. ( _I |` A ) -> y e. R ) <-> A. x e. A x R x ) |
18 |
1 17
|
bitri |
|- ( ( _I |` A ) C_ R <-> A. x e. A x R x ) |